Proof assistants are getting more widespread use in research and industry to provide certified and independently checkable guarantees about theories, designs, systems and implementations. However, proof assistant implementations themselves are seldom verified, although they take a major share of the trusted code base in any such certification effort. In this area, proof assistants based on Higher-Order Logic enjoy stronger guarantees, as self-certified implementations have been available for some years. One cause of this difference is the inherent complexity of dependent type theories together with their extensions with inductive types, universe polymorphism and complex sort systems, and the gap between theory on paper and practical implementations in efficient programming languages. MetaCoq is a collaborative project that aims to tackle these difficulties to provide the first fully-certified realistic implementation of a type checker for the full calculus underlying the Coq proof assistant. To achieve this, we refined the sometimes blurry, if not incorrect, specification and implementation of the system. We show how theoretical tools from this community such as bidirectional type-checking, Tait-Martin-Lof/Takahashis confluence proof technique and monadic and dependently-typed programming can help construct the following artefacts: a specification of Coqs syntax and type theory, the Polymorphic Cumulative Calculus of (Co)-Inductive Constructions (PCUIC); a monad for the manipulation of raw syntax and interaction with the Coq system; a verification of PCUICs metatheory, whose main results are the confluence of reduction, type preservation and principality of typing; a realistic, correct and complete type-checker for PCUIC; a sound type and proof erasure procedure from PCUIC to untyped lambda-calculus, i.e., the core of the extraction mechanism of Coq.
Download