Skip to content

MetaCoq 1.1 for Coq 8.16
Compare
Choose a tag to compare
@mattam82 mattam82 released this 22 Sep 12:47
v1.1-8.16
aa72b60

We are happy to announce release 1.1 of the MetaCoq project for Coq 8.16, available both as source and through opam. See the website for a detailed overview of the project, introductory material and related articles and presentations.

This new version integrates:

  • Support for primitive integers and floating point values, using the same typechecking mechanism as Coq's kernel, up to the erased lambda-box language.
  • Better computational behavior of the safe checker.
  • Support for nix and cachix (useful for CI, allows to reuse remotely compiled components)
  • Registering of projections for inductive types defined as records
  • More efficient eta-expansion transformation using environment maps instead of association lists.

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