Correct and Complete Type Checking and Certified Erasure for <scp>Coq</scp> , in <scp>Coq</scp>

<jats:p> <jats:sc>Coq</jats:sc> is built around a well-delimited kernel that performs type checking for definitions in a variant of the Calculus of Inductive Constructions ( <jats:sc>CIC</jats:sc> ). Although the metatheory of <jats:sc>CIC</jats:sc> is very stable and reliable, the correctness of its implementation in <jats:sc>Coq</jats:sc> is less clear. Indeed, implementing an efficient type checker for <jats:sc>CIC</jats:sc> 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 <jats:sc>Coq</jats:sc> . This article presents the first implementation of a type checker for the kernel of <jats:sc>Coq</jats:sc> (without the module system, template polymorphism and η-conversion), which is proven sound and complete in <jats:sc>Coq</jats:sc> with respect to its formal specification. Note that because of Gödel’s second incompleteness theorem, there is no hope to prove completely the soundness of the specification of <jats:sc>Coq</jats:sc> inside <jats:sc>Coq</jats:sc> (in particular strong normalization), but it is possible to prove the correctness and completeness of the implementation assuming soundness of the specification, thus moving from a trusted code base (TCB) to a trusted theory base (TTB) paradigm. Our work is based on the <jats:sc>MetaCoq</jats:sc> project which provides meta-programming facilities to work with terms and declarations at the level of the kernel. We verify a relatively efficient type checker based on the specification of the typing relation of the Polymorphic, Cumulative Calculus of Inductive Constructions ( <jats:sc>PCUIC</jats:sc> ) at the basis of <jats:sc>Coq</jats:sc> . It is worth mentioning that during the verification process, we have found a source of incompleteness in <jats:sc>Coq</jats:sc> ’s official type checker, which has then been fixed in <jats:sc>Coq</jats:sc> 8.14 thanks to our work. In addition to the kernel implementation, another essential feature of <jats:sc>Coq</jats:sc> is the so-called <jats:italic>extraction</jats:italic> mechanism: the production of executable code in functional languages from <jats:sc>Coq</jats:sc> 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 <jats:sc>Coq</jats:sc> in the future. </jats:p>

@article{sozeau2025,
  title = {{Correct and Complete Type Checking and Certified Erasure for
            <scp>Coq</scp>
            , in
            <scp>Coq</scp>}},
  author = {Matthieu Sozeau and Yannick Forster and Meven Lennon-Bertrand and Jakob Nielsen and Nicolas Tabareau and Théo Winterhalter},
  journal = {Journal of the ACM},
  volume = {72},
  issue = {1},
  year = 2025,
  month = 1,
  day = 27,
  doi = {10.1145/3706056},
}