The MetaCoq Project - Archive ouverte HAL Access content directly
Journal Articles Journal of Automated Reasoning Year : 2020

The MetaCoq Project

(1) , (2) , (3) , (4) , (5) , (5) , (2) , (3) , (3)
1
2
3
4
5

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.
Fichier principal
Vignette du fichier
The_MetaCoq_Project.pdf (618.17 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02167423 , version 1 (27-06-2019)

Identifiers

Cite

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

Altmetric

Share

Gmail Facebook Twitter LinkedIn More