Skip to content

MetaCoq 1.2 for Coq 8.17
Compare
Choose a tag to compare
@mattam82 mattam82 released this 21 Apr 16:17
· 195 commits to coq-8.17 since this release
v1.2-8.17
1f9ed65

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

The main changes in this new version are (w.r.t. v1.1.1):

  • A cleaned-up abstract environment structure for the implementation of the verified type-checker and cleaned-up canonicity and consistency theorems by @tabareau.
  • A new quotation library with a work-in-progress proof of Löb's theorem by @JasonGross.
  • An integration of the typed erasure phase of the ConCert project by @annenkov and @mattam82.
    Beware, adaptation of the correctness proof is not finished and it is not integrated in the extracted pipeline of MetaCoq Erase yet.
  • Reorganization of the packages, separating plugins from theories by @tabareau.

The preprint "Correct and Complete Type Checking and Certified Erasure for Coq, in Coq" presents the development of the sound and complete type checker based on bidirectional typing, the meta-theoretical results (subject reduction, standardization, canonicity and consistency) and the verified erasure procedure of this version of MetaCoq.

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, sound and complete type checker for PCUIC, a verified type and proof erasure procedure from PCUIC to untyped lambda calculus and a quotation library. 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 using opam install coq-metacoq.
This release will be included in an upcoming Coq Platform.

The current release includes several subpackages, which can be compiled and installed separately if desired:

  • the utils library contains extensions to the standard library (notably for reasoning with All/All-n type-valued predicates) (in directory utils, and as coq-metacoq-utils).
  • the common libraries of basic definitions for the abstract syntax trees shared by multiple languages (common, coq-metacoq-common)
  • the Template-Coq quoting library and plugin (template-coq / coq-metacoq-template)
  • a formalisation of meta-theoretical properties of PCUIC, the calculus underlying Coq (pcuic / coq-metacoq-pcuic)
  • a verified equivalence between Template-Coq and PCUIC typing (in directory template-pcuic and as coq-metacoq-template-pcuic)
  • a total verified type-checker for Coq (safechecker / coq-metacoq-safechecker), usable inside Coq.
  • a plugin interfacing with the extracted type-checker in OCaml, providing the MetaCoq SafeCheck <term> command (safechecker-plugin, coq-metacoq-safechecker-plugin)
  • a verified type and proof erasure function for Coq (erasure / coq-metacoq-erasure), usable inside Coq.
  • a plugin interfacing with the extracted erasure pipeline in OCaml, providing the MetaCoq Erase <term> command (erasure-plugin, coq-metacoq-erasure-plugin)
  • a quoting library, allowing the quotation of terms and type derivations along with associated data structures as ASTs/terms (quotation / coq-metacoq-quotation).
  • 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, Jason Gross, 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

What's Changed

New Contributors

Full Changelog: v1.1.1-8.16...v1.2-8.17

Contributors

kyoDralliam, mattam82, and 6 other contributors
Assets 2
Loading