The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

Dear Coq-Clubbers,

  we are happy to announce the first alpha release of the [MetaCoq project](https://metacoq.github.io/metacoq/) 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](https://github.com/MetaCoq/metacoq) 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-coq` and as `coq-metacoq-template`)
- a partial type-checker for Coq (`checker` / `coq-metacoq-checker`), usable as `MetaCoq 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 as `MetaCoq SafeCheck test`
- a verified type and proof erasure function for Coq (`erasure` / `coq-metacoq-erasure`), usable as `MetaCoq Erase test`
- a set of example translations from Type Theory to Type Theory (`translation`/ `coq-metacoq-translations`).

A good place to start are the files `demo.v`, `safechecker_test.v`, `erasure_test.v` in the `test-suite` directory.

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](https://github.com/MetaCoq/metacoq/issues) or [asking questions on gitter](https://gitter.im/coq/metacoq).

Enjoy!

The MetaCoq Team