Martin-L\"of \`a la Coq
Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard and, Pierre-Marie P\'edrot, Lo\"ic Pujet

TL;DR
This paper provides a comprehensive mechanization of Martin-Löf Type Theory in Coq, including a certified type checker, by extending prior work with a focus on decidability and modular formalization.
Contribution
It introduces a formalized, executable type checker for MLTT in Coq, demonstrating decidability of type checking without impredicativity or additional axioms.
Findings
Decidability of conversion and type checking established
Certified, executable type checker implemented in Coq
Modular formalization leveraging Coq's features
Abstract
We present an extensive mechanization of the meta-theory of Martin-L\"of 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 , , , 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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Semantic Web and Ontologies
