Skip to Main content Skip to Navigation
Journal articles

The MetaCoq Project

Matthieu Sozeau 1 Abhishek Anand 2 Simon Boulier 3 Cyril Cohen 4 Yannick Forster 5 Fabian Kunze 5 Gregory Malecha 2 Nicolas Tabareau 3 Théo Winterhalter 3
1 PI.R2 - Design, study and implementation of languages for proofs and programs
CNRS - Centre National de la Recherche Scientifique, Inria de Paris, UP - Université de Paris, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale
3 GALLINETTE - Gallinette : vers une nouvelle génération d'assistant à la preuve
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
4 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : The MetaCoq project aims to provide a certified meta-programming environment in Coq. It builds on Template-Coq, a plugin for Coq originally implemented by Malecha (2014), which provided a reifier for Coq terms and global declarations, as represented in the Coq kernel, as well as a denotation command. Recently, it was used in the CertiCoq certified compiler project (Anand et al., 2017), as its front-end language, to derive parametricity properties (Anand and Morrisett, 2018). However, the syntax lacked semantics, be it typing semantics or operational semantics, which should reflect, as formal specifications in Coq, the semantics of Coq's type theory itself. The tool was also rather bare bones, providing only rudimentary quoting and unquoting commands. We generalize it to handle the entire Polymorphic Calculus of Cumulative Inductive Constructions (pCUIC), as implemented by Coq, including the kernel's declaration structures for definitions and inductives, and implement a monad for general manipulation of Coq's logical environment. We demonstrate how this setup allows Coq users to define many kinds of general purpose plugins, whose correctness can be readily proved in the system itself, and that can be run efficiently after extraction. We give a few examples of implemented plugins, including a parametricity translation and a certifying extraction to call-by-value λ-calculus. We also advocate the use of MetaCoq as a foundation for higher-level tools.
Document type :
Journal articles
Complete list of metadatas

Cited literature [34 references]  Display  Hide  Download

https://hal.inria.fr/hal-02167423
Contributor : Matthieu Sozeau <>
Submitted on : Thursday, June 27, 2019 - 6:11:12 PM
Last modification on : Wednesday, June 24, 2020 - 4:19:53 PM

File

The_MetaCoq_Project.pdf
Files produced by the author(s)

Identifiers

Citation

Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, et al.. The MetaCoq Project. Journal of Automated Reasoning, Springer Verlag, 2020, ⟨10.1007/s10817-019-09540-0⟩. ⟨hal-02167423⟩

Share

Metrics

Record views

424

Files downloads

883