POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Tue 16 Jan 2024 10:00 - 10:30 at Kelvin Lecture - Interactive Proof Development Chair(s): Brigitte Pientka

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 Π, Σ, ℕ, and Id 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. We also investigate how to take advantage of the features of Coq, especially universe polymorphism and the meta-programming facilities provided by tactics.

Tue 16 Jan

Displayed time zone: London change

09:00 - 10:30
Interactive Proof Development CPP at Kelvin Lecture
Chair(s): Brigitte Pientka McGill University
Improved Assistance for Interactive Proof
Cezary Kaliszyk University of Innsbruck
Martin-Löf à la Coqdistinguished paper
Arthur Adjedj ENS Paris Saclay, Université Paris-Saclay, Meven Lennon-Bertrand University of Cambridge, Kenji Maillard INRIA, Pierre-Marie Pédrot INRIA, Loïc Pujet Stockholm University