Type-checking kernels of modern proof assistants based on type theories have become very complex, with over tens of thousands of lines of code, and thus error-prone. How can we build certified type checking kernels that we can trust? – We propose a correct-by-construction way to develop proof assistants and describe McTT, a bottom-up, certified implementation of Martin-Löf type theory (MLTT) in Coq. McTT is composed of two major parts: the theoretical component and the executable component. In the theoretical component, we formalize a version of MLTT that has a full cumulative universe hierarchy. We prove soundness and completeness of our normalization-by-evaluation algorithm and thus derive the logical consistency of the system using an untyped domain model. In addition to the theoretical component which formalizes a richer type theory than previous mechanization efforts, another key contribution in McTT is the executable component. In this component, we provide a proven-correct type-checker eventually extracted into OCaml. The extracted code is of high quality; it is identical to what a skilled human programmer would have written, and thus the resulting executable is also efficient.

McTT provides the a basic framework for certified implementations of dependent type theories and is open to many possible future extensions.