一句话：在 Coq 中形式化验证 Coq 内核的类型检查器与类型/证明擦除，将可信代码基缩小为可信理论基。
Coq 的内核类型检查器实现复杂、依赖隐式不变量，平均每年出现关键 bug；提取中的类型与证明擦除也很微妙。本文基于 MetaCoq，对作为 Coq 基础的 PCUIC 类型关系给出形式规约，实现相对高效且可靠的类型检查器，并在 Coq 中证明其相对于该规约与部分元理论公理的正确性。由于哥德尔不完备定理，无法在 Coq 内证明规约本身的完全正确性，因此该方法将可信代码基（TCB）转为可信理论基（TTB）。作者还验证了类型与证明擦除步骤，从而支持安全类型检查器的经验证提取。这是首个针对 Coq 内核（不含模块系统与模板多态）的经验证类型检查器实现。
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.
@article{paperbot510,
title = {Coq Coq correct! verification of type checking and erasure for Coq, in Coq},
author = {Matthieu Sozeau and Simon Boulier and Yannick Forster and Nicolas Tabareau and Théo Winterhalter},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371076}
}