MetaCoq 1.2 release

Announcements
1

Dear Coq and MetaCoq users,

We are happy to announce that version 1.2 of the MetaCoq project has been released for Coq 8.16 and Coq 8.17, available both as source and through opam. It will also be part of the next Coq Platform. 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 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.

1 Like
2

Thanks for the hard work everyone, this is an amazing piece of work!

1 Like