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.

• Download: metalib-20090714.zip

Previous versions

We list these in reverse chronological order.

• metalib-20090321.zip
  • Compatible with Coq 8.2
• metalib-oregon08-tutorial.zip
  • Compatible with Coq 8.1
  • Originally distributed at the 2008 Oregon Summer School on Logic and Theorem Proving in Programming Languages as part of the course on Coq for Programming Language Metatheory.
• metalib-popl08-tutorial.zip
  • Compatible with Coq 8.1
  • Originally distributed at POPL 2008 for the tutorial Using Proof Assistants for Programming Language Research (or, How to write your next POPL paper in Coq).
• metalib-popl08-paper.zip
  • Compatible with Coq 8.1
  • Originally distributed with the paper Engineering Formal Metatheory, which appeared at POPL 2008. This code can also be found on Arthur Charguéraud's site.

Contact

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