2 papers
cs.PL2023
Martin-Löf à la Coq
Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard +2
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 no…
cs.PL2023
Definitional Functoriality for Dependent (Sub)Types -- Extended version
Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard
Dependently typed proof assistant rely crucially on definitional equality, which relates types and terms that are automatically identified in the underlying type theory. This paper…