Martin-L\"of \`a la Coq

• DOI: 10.48550/arxiv.2310.06376
• Publication Date: 2024-01-09
• Authors: Adjedj, Arthur; Lennon-Bertrand, ...; Maillard, Kenji; Pédrot, Pierre-Marie; Pujet, Loïc
• Keywords: FOS: Computer and information sciences; Computer Science - Logic in Computer Science; D.3.1; [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]; [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]; Computer Science - Programming Languages; 5003 Philosophy; [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]; 4904 Pure Mathematics; Dependent type system; [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]; Logic in Computer Science (cs.LO); 46 Information and Computing Sciences; 50 Philosophy and Religious Studies; 49 Mathematical Sciences; F.3.2; F.4.1; F.3.3; Logical relations; D.3.1; F.3.2; F.3.3; F.4.1; 4612 Software Engineering; Bidirectional typing; Programming Languages (cs.PL)

We present an extensive mechanization of the meta-theory of Martin-Löf Type Theory (MLTT) in the Coq proof assistant. Our development builds on pre-existing work in Agda to show not only the decidability of conversion, but also the decidability of type checking, using an approach guided by bidirectional type checking. From our proof of decidability, we obtain a certified and executable type checker for a full-fledged version of MLTT with support for $Π$, $Σ$, $\mathbb{N}$, and identity types, and one universe. Furthermore, our development does not rely on impredicativity, induction-recursion or any axiom beyond MLTT with a schema for indexed inductive types and a handful of predicative universes, narrowing the gap between the object theory and the meta-theory to a mere difference in universes. Finally, we explain our formalization choices, geared towards a modular development relying on Coq's features, e.g. meta-programming facilities provided by tactics and universe polymorphism.