McTT: Building A Correct-By-Construction Proof Checker For Martin-Löf Type Theory

This conference talk presents McTT, a certified implementation of Martin-Löf type theory (MLTT) in Coq that builds a correct-by-construction proof checker. Learn how researchers from McGill University and Amazon Web Services address the challenge of creating trustworthy type-checking kernels for proof assistants, which have become increasingly complex and error-prone. Discover their bottom-up approach that includes both theoretical and executable components, featuring a formalized version of MLTT with a full cumulative universe hierarchy. The presentation explains how they proved soundness and completeness of their normalization-by-evaluation algorithm, derived logical consistency using an untyped domain model, and created a proven-correct type-checker that extracts into high-quality, efficient OCaml code. This 36-minute talk from the WITS 2025 workshop provides a foundational framework for certified implementations of dependent type theories and discusses potential future extensions.