Skip to Main content Skip to Navigation
Journal articles

Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq

Matthieu Sozeau 1 Simon Boulier 2, 3 Yannick Forster 4 Nicolas Tabareau 2, 3 Théo Winterhalter 3, 2
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
2 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
Abstract : Coq is built around a well-delimited kernel that perfoms typechecking for definitions in a variant of the Calculus of Inductive Constructions (CIC). Although the metatheory of CIC is very stable and reliable, the correctness of its implementation in Coq is less clear. Indeed, implementing an efficient type checker for CIC is a rather complex task, and many parts of the code rely on implicit invariants which can easily be broken by further evolution of the code. Therefore, on average, one critical bug has been found every year in Coq. This paper presents the first implementation of a type checker for the kernel of Coq (without the module system and template polymorphism), which is proven correct in Coq with respect to its formal specification and axiomatisation of part of its metatheory. Note that because of Gödel's incompleteness theorem, there is no hope to prove completely the correctness of the specification of Coq inside Coq (in particular strong normalisation or canonicity), but it is possible to prove the correctness of the implementation assuming the correctness of the specification, thus moving from a trusted code base (TCB) to a trusted theory base (TTB) paradigm. Our work is based on the MetaCoq project which provides metaprogramming facilities to work with terms and declarations at the level of this kernel. Our type checker is based on the specification of the typing relation of the Polymorphic, Cumulative Calculus of Inductive Constructions (PCUIC) at the basis of Coq and the verification of a relatively efficient and sound type-checker for it. In addition to the kernel implementation, an essential feature of Coq is the so-called extraction: the production of executable code in functional languages from Coq definitions. We present a verified version of this subtle type-and-proof erasure step, therefore enabling the verified extraction of a safe type-checker for Coq.
Complete list of metadatas

Cited literature [51 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-02380196
Contributor : Théo Winterhalter <>
Submitted on : Wednesday, December 11, 2019 - 3:01:24 PM
Last modification on : Tuesday, January 5, 2021 - 4:26:24 PM

File

popl20main-p34-p-79d1b9f-43140...
Files produced by the author(s)

Identifiers

Citation

Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter. Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq. Proceedings of the ACM on Programming Languages, ACM, 2020, pp.1-28. ⟨10.1145/3371076⟩. ⟨hal-02380196v2⟩

Share

Metrics

Record views

487

Files downloads

1146