MetaCoq

MetaCoq

Build status MetaCoq Chat Open in Visual Studio Code

MetaCoq is a project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins (i.e. translations, compilers or tactics) in Coq.

Quick jump

Getting started

Installation instructions

See INSTALL.md

Documentation

See DOC.md

Overview of the project

At the center of this project is the Template-Coq quoting library for Coq. The project currently has a single repository extending Template-Coq with additional features. Each extension is in a dedicated folder. The dependency graph might be useful to navigate the project. Statistics: ~300kLoC of Coq, ~30kLoC of OCaml.

Template-Coq

Template-Coq is a quoting library for Coq. It takes Coq terms and constructs a representation of their syntax tree as an inductive data type. The representation is based on the kernel’s term representation.

After importing MetaCoq.Template.Loader there are commands MetaCoq Test Quote t., MetaCoq Quote Definition name := (t). and MetaCoq Quote Recursively Definition name := (t). as well as a tactic quote_term t k, where in all cases t is a term and k a continuation tactic.

In addition to this representation of terms, Template Coq includes:

PCUIC

PCUIC, the Polymorphic Cumulative Calculus of Inductive Constructions is a cleaned up version of the term language of Coq and its associated type system, shown equivalent to the one of Coq. This version of the calculus has proofs of standard metatheoretical results:

See the PCUIC README for a detailed view of the development.

Safe Checker

Implementation of a fuel-free and verified reduction machine, conversion checker and type checker for PCUIC. This relies on a postulate of strong normalization of the reduction relation of PCUIC on well-typed terms. The checker is shown to be correct and complete w.r.t. the PCUIC specification. The extracted safe checker is available in Coq through a new vernacular command:

MetaCoq SafeCheck <term>

After importing MetaCoq.SafeChecker.Loader.

To roughly compare the time used to check a definition with Coq’s vanilla type-checker, one can use:

MetaCoq CoqCheck <term>

This also includes a verified, efficient re-typing procedure (useful in tactics) in MetaCoq.SafeChecker.PCUICSafeRetyping.

See the SafeChecker README for a detailed view of the development.

Erasure

An erasure procedure to untyped lambda-calculus accomplishing the same as the type and proof erasure phase of the Extraction plugin of Coq. The extracted safe erasure is available in Coq through a new vernacular command:

MetaCoq Erase <term>

After importing MetaCoq.Erasure.Loader.

The erasure pipeline includes verified optimizations to remove lets in constructors, remove cases on propositional terms, switch to an unguarded fixpoint reduction rule and transform the higher-order constructor applications to first-order blocks for easier translation to usual programming languages. See the erasure README for a detailed view of the development.

Translations

Examples of translations built on top of this:

Quotation

The Quotation module is geared at providing functions □T → □□T for □T := Ast.term (currently implemented) and for □T := { t : Ast.term & Σ ;;; [] |- t : T } (still in the works).

Ultimately the goal of this development is to prove that is a lax monoidal semicomonad (a functor with cojoin : □T → □□T that codistributes over unit and ×), which is sufficient for proving Löb’s theorem.

The public-facing interface of this development is provided in MetaCoq.Quotation.ToTemplate.All and MetaCoq.Quotation.ToPCUIC.All.

See the Quotation README for a more detailed view of the development.

Examples

Papers

Team & Credits

Abhishek Anand Danil Annenkov Simon Boulier
Cyril Cohen Yannick Forster Jason Gross
Meven Lennon-Bertrand Kenji Maillard Gregory Malecha
Jakob Botsch Nielsen Matthieu Sozeau Nicolas Tabareau
Théo Winterhalter
MetaCoq is developed by (left to right) Abhishek Anand, Danil Annenkov, Simon Boulier, Cyril Cohen, Yannick Forster, Jason Gross, Meven Lennon-Bertrand, Kenji Maillard, Gregory Malecha, Jakob Botsch Nielsen, Matthieu Sozeau, Nicolas Tabareau and Théo Winterhalter.

Copyright (c) 2014-2023 Gregory Malecha
Copyright (c) 2015-2023 Abhishek Anand, Matthieu Sozeau
Copyright (c) 2017-2023 Simon Boulier, Nicolas Tabareau, Cyril Cohen
Copyright (c) 2018-2023 Danil Annenkov, Yannick Forster, Théo Winterhalter
Copyright (c) 2020-2023 Jakob Botsch Nielsen, Meven Lennon-Bertrand
Copyright (c) 2022-2023 Kenji Maillard
Copyright (c) 2023      Jason Gross

This software is distributed under the terms of the MIT license. See LICENSE for details.

Bugs

Please report any bugs or feature requests on the github issue tracker.