Skip to content

MetaCoq 1.0 for Coq 8.16
Compare
Choose a tag to compare
@mattam82 mattam82 released this 01 Jul 12:47
v1.0-8.16
5668361

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 template-coq and as coq-metacoq-template)
  • 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 inside Coq or extracted to OCaml as MetaCoq SafeCheck <term>
  • a verified type and proof erasure function for Coq (erasure / 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 (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, 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

Assets 2
Loading