Martin-Löf Type Theory Mechanization in Coq

Explore an extensive mechanization of Martin-Löf Type Theory (MLTT) metatheory in the Coq proof assistant through this 30-minute conference talk presented at CPP 2024. Delve into the work of Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, and Loïc Pujet as they demonstrate the decidability of conversion and type checking using a bidirectional approach. Discover how their development yields a certified, executable type checker for a comprehensive version of MLTT, supporting Π, Σ, ℕ, and Id types with one universe. Learn about their formalization choices aimed at creating a modular development leveraging Coq's features like universe polymorphism and metaprogramming with tactics. Gain insights into how this work narrows the gap between object theory and metatheory, relying only on MLTT extended with indexed inductive types and predicative universes.