MetaCoq
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
 Documentation
 Overview of the project
 Papers
 Related Projects
 Team & Credits
 Bugs
Getting started

You may want to start with a demo.

The current branch documentation (as light coqdoc files).

The overview of the different parts of the project.
Installation instructions
See INSTALL.md
Documentation
See DOC.md
Overview of the project
At the center of this project is the TemplateCoq quoting library for Coq. The project currently has a single repository extending TemplateCoq 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.
TemplateCoq
TemplateCoq 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:

Reification of the environment structures, for constant and inductive declarations along with their universe structures.

Denotation of terms and global declarations.

A monad for querying the environment, manipulating global declarations, calling the type checker, and inserting them in the global environment, in the style of MTac. Monadic programs
p : TemplateMonad A
can be run usingMetaCoq Run p
. 
A formalization of the typing rules reflecting the ones of Coq, covering all of Coq except etaexpansion and template polymorphism.
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:

Weakening for global declarations, weakening and substitution for local contexts.

Confluence of reduction using a notion of parallel reduction

Context cumulativity / conversion and validity of typing.

Subject Reduction (case/cofix reduction excluded)

Principality: every typeable term has a smallest type.

Bidirectional presentation: an equivalent presentation of the system that enforces directionality of the typing rules. Strengthening follows from this presentation.

Elimination restrictions: the elimination restrictions ensure that singleton elimination (from Prop to Type) is only allowed on singleton inductives in Prop.

Canonicity: The weak head normal form of a term of inductive type is a constructor application.

Consistency under the assumption of strong normalization

Weak callbyvalue standardization: Normal forms of terms of firstorder inductive type can be found via weak callbyvalue evaluation.
See the PCUIC README for a detailed view of the development.
Safe Checker
Implementation of a fuelfree 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 welltyped 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 typechecker, one can use:
MetaCoq CoqCheck <term>
This also includes a verified, efficient retyping 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 lambdacalculus 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 higherorder constructor applications to firstorder 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:

a parametricity plugin in translations/param_original.v

a plugin to negate functional extensionality in translations/times_bool_fun.v
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 publicfacing 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

An example Coq plugin built on the Template Monad, which can be used to add a constructor to any inductive type is in examples/add_constructor.v

An example extracted Coq plugin built on the extractable Template Monad, which can be used to derive lenses associated to a record type is in testsuite/plugindemo. The plugin runs in OCaml and is a template for writing extracted plugins.

An example
constructor
tactic written using the Template Monad is in examples/constructor_tac.v, and a more elaborate verified tautology checker is in examples/tauto.v. 
The testsuite files testsuite/erasure_test.v and testsuite/safechecker_test.v show example uses (and current limitations of) the extracted verified checker and erasure.

The testsuite/self_erasure.v file checks that erasure works on the verified typechecking and erasure programs themselves.

The testsuite file testsuite/erasure_live_test.v shows uses of the verified erasure running inside Coq.
Papers

“Correct and Complete Type Checking and Certified Erasure for Coq, in Coq” Matthieu Sozeau, Yannick Forster, Meven LennonBertrand, Nicolas Tabareau and Théo Winterhalter. Submitted. April 2023.
This paper presents the whole metatheoretical development of PCUIC and verified typechecking and erasure, as of version 1.2 of MetaCoq.

“The Curious Case of Case” Matthieu Sozeau, Meven LennonBertrand and Yannick Forster. WITS 2022 presentation, Philadelphia. This presents the challenges around the representation of cases in Coq and PCUIC.

“Bidirectional Typing for the Calculus of Inductive Constructions” Meven LennonBertrand, PhD thesis, June 2022. Part 2 describes in detail the bidirectional variant of typing and its use to verify correctness and completeness of the type checker.

“Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq” Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau and Théo Winterhalter. POPL 2020, New Orleans.
This paper presented the formal proofs of soundness of conversion, type checking and erasure. Now superseded by the April 2023 article above.

“Formalization and metatheory of type theory” Théo Winterhalter, PhD thesis, September 2020. Part 3 describes in detail the verified reduction, conversion and type checker.

“Coq Coq Codet! Towards a Verified Toolchain for Coq in MetaCoq” Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau and Théo Winterhalter. Abstract and presentation given at the Coq Workshop 2019, September 2019.

“The MetaCoq Project” Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau and Théo Winterhalter. JAR, February 2020. Extended version of the ITP 2018 paper.
This includes a full documentation of the Template Monad and the typing rules of PCUIC.

A certifying extraction with time bounds from Coq to callbyvalue λcalculus. Yannick Forster and Fabian Kunze. ITP 2019. Example

“Towards Certified MetaProgramming with Typed TemplateCoq” Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau and Nicolas Tabareau. ITP 2018.

The system was presented at Coq’PL 2018
Related Projects

The CertiCoq project develops a certified compiler from the output of verified erasure down to CompCert Clight. It provides in particular OCaml and fully foundationally verified plugins for the whole compilation pipeline from Gallina to Clight and the verified typechecker of MetaCoq.

The ConCert project develops certified or certifying compilers from Gallina to smart contract languages (Liquidity and CameLIGO), the functional language Elm, and a subset of the Rust programming languages. It uses the typed erasure variant to gather more type information about erased terms and perform optimizations based on this information. The project focuses in particular on the verification and safe extraction of smart contracts for blockchains.
Team & Credits
MetaCoq is developed by (left to right)
Abhishek Anand,
Danil Annenkov,
Simon Boulier,
Cyril Cohen,
Yannick Forster,
Jason Gross,
Meven LennonBertrand,
Kenji Maillard,
Gregory Malecha,
Jakob Botsch Nielsen,
Matthieu Sozeau,
Nicolas Tabareau and
Théo Winterhalter.
Copyright (c) 20142023 Gregory Malecha
Copyright (c) 20152023 Abhishek Anand, Matthieu Sozeau
Copyright (c) 20172023 Simon Boulier, Nicolas Tabareau, Cyril Cohen
Copyright (c) 20182023 Danil Annenkov, Yannick Forster, Théo Winterhalter
Copyright (c) 20202023 Jakob Botsch Nielsen, Meven LennonBertrand
Copyright (c) 20222023 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.