Martin-Löf à la Coq
In: https://hal.science/hal-04214008 ; 2024, 2024
Online
report
Zugriff:
Keywords: Dependent type systems, Bidirectional typing, Logical relations ; We present an extensive mechanization of the metatheory 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. Our development does not rely on impredicativity, induction-recursion or any axiom beyond MLTT extended with indexed inductive types and a handful of predicative universes, thus narrowing the gap between the object theory and the metatheory to a mere difference in universes. Furthermore, our formalization choices are geared towards a modular development that relies on Coq's features, e.g. universe polymorphism and metaprogramming with tactics.
Titel: |
Martin-Löf à la Coq
|
---|---|
Autor/in / Beteiligte Person: | Adjedj, Arthur ; Lennon-Bertrand, Meven ; Maillard, Kenji ; Pédrot, Pierre-Marie ; Pujet, Loïc ; Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay) ; Paris-Saclay, Université ; Computer Laboratory Cambridge ; University of Cambridge UK (CAM) ; Gallinette : vers une nouvelle génération d'assistant à la preuve (GALLINETTE) ; Inria Rennes – Bretagne Atlantique ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique) ; Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT)-NANTES UNIVERSITÉ - École Centrale de Nantes (Nantes Univ - ECN) ; Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes université - UFR des Sciences et des Techniques (Nantes univ - UFR ST) ; Nantes Université - pôle Sciences et technologie ; Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes Université - pôle Sciences et technologie ; Nantes Université (Nantes Univ)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique) ; Nantes Université (Nantes Univ) ; Laboratoire des Sciences du Numérique de Nantes (LS2N) ; University, Stockholm |
Link: | |
Zeitschrift: | https://hal.science/hal-04214008 ; 2024, 2024 |
Veröffentlichung: | HAL CCSD, 2024 |
Medientyp: | report |
DOI: | 10.1145/3636501.3636951 |
Schlagwort: |
|
Sonstiges: |
|