We are happy to announce the first alpha release of the MetaCoq project for Coq 8.8 and 8.9, available both as sources and as opam packages (from the released repository).
MetaCoq was formerly called Template-Coq, but now also includes a (work-in-progress) formalisation of Coq in Coq, a verified type checker for Coq, and a verified type and proof erasure procedure, besides the tools for manipulating Coq terms and developing certified plugins (i.e. translations, compilers or tactics) in Coq provided by Template-Coq.
You can install it directly from sources or by typing opam install coq-metacoq.
The current release includes several subpackages, which can be compiled and installed separately if wanted:
- the Template-Coq quoting library (in directory
template-coqand ascoq-metacoq-template) - a partial type-checker for Coq (
checker/coq-metacoq-checker), usable asMetaCoq Check test. - a formalisation of meta-theoretical properties of PCUIC, the calculus underlying Coq (
pcuic/coq-metacoq-pcuic) - a total verified type-checker for Coq (
safechecker/coq-metacoq-safechecker), usable asMetaCoq SafeCheck test - a verified type and proof erasure function for Coq (
erasure/coq-metacoq-erasure), usable asMetaCoq Erase test - a set of example translations from Type Theory to Type Theory (
translation/coq-metacoq-translations).
A good place to start are the filesdemo.v,safechecker_test.v,erasure_test.vin thetest-suitedirectory.
MetaCoq is developed by Abhishek Anand, Danil Annenkov, Simon Boulier, Cyril Cohen, Yannick Forster, Gregory Malecha, Matthieu Sozeau, Nicolas Tabareau and Théo Winterhalter.
Please contribute by opening issues or asking questions on gitter.
Enjoy!
The MetaCoq Team