We are happy to announce release 1.0 of the MetaCoq project for Coq 8.14, 8.15, and 8.16, available both as sources and as opam packages. See the website for a detailed overview of the project, introductory material and related articles and presentations.
MetaCoq integrates Template-Coq, a reification and denotation plugin for Coq terms and global declarations, a Template monad for metaprogramming (including the ability to extract these metaprograms to OCaml for efficiency), a formalisation of Coq’s calculus PCUIC in Coq, a relatively efficient, correct and complete type checker for PCUIC, and a verified type and proof erasure procedure from PCUIC to untyped lambda calculus. MetaCoq provides a low-level interface to develop certified plugins like translations, compilers or tactics in Coq itself.
You can install MetaCoq directly from sources or by typing
opam install coq-metacoq.
This release will also be included in an upcoming Coq Platform.
The current release includes several subpackages, which can be compiled and installed separately if desired:
- the Template-Coq quoting library (in directory
- a formalisation of meta-theoretical properties of PCUIC, the calculus underlying Coq (
- a total verified type-checker for Coq (
coq-metacoq-safechecker), usable inside Coq or extracted to OCaml as
MetaCoq SafeCheck <term>
- a verified type and proof erasure function for Coq (
coq-metacoq-erasure), usable inside Coq or extracted to OCaml as
MetaCoq Erase <term>
- a set of example translations from Type Theory to Type Theory (
A good place to start are the files
erasure_test.v in the
MetaCoq is developed by Abhishek Anand, Danil Annenkov, Jakob Botsch Nielsen, Simon Boulier, Cyril Cohen, Yannick Forster, Meven Lennon-Bertrand, Kenji Maillard, Gregory Malecha, Matthieu Sozeau, Nicolas Tabareau, and Théo Winterhalter. You are welcome to contribute by opening issues and PRs. A MetaCoq Zulip stream is also available.
The MetaCoq Team