Metatheory library - Home

The Penn PLClub has developed, and continues to work on, a collection of Coq libraries for mechanizing programming language metatheory in the Coq proof assistant. The original design and implementation of the library includes work by Arthur Charguéraud and was distributed with Engineering Formal Metatheory. The library has evolved since then, but its purpose has remained the same.

Current version: 20090714 (for Coq 8.2)

The current version includes a short introduction to Coq and a tutorial on using the library. It comes with a README file and documentation (including installation instructions). A complete change log is also available.

Previous versions

We list these in reverse chronological order.


If you have any questions about the library, feel free to contact Brian Aydemir.