Eliminating Reflection from Type Theory ; Eliminating Reflection from Type Theory: To the Legacy of Martin Hofmann
In: CPP 2019 - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs ; https://hal.science/hal-01849166 ; CPP 2019 - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2019, Lisbonne, Portugal. pp.91-103, ⟨10.1145/3293880.3294095⟩ ; https://popl19.sigplan.org/track/CPP-2019, 2019
Online
Konferenz
Zugriff:
International audience ; Type theories with equality reflection, such as extensional type theory (ETT), are convenient theories in which to formalise mathematics, as they make it possible to consider provably equal terms as convertible. Although type-checking is undecidable in this context, variants of ETT have been implemented, for example in NuPRL and more recently in Andromeda. The actual objects that can be checked are not proof-terms, but derivations of proof-terms. This suggests that any derivation of ETT can be translated into a typecheckable proof term of intensional type theory (ITT). However, this result, investigated categorically by Hofmann in 1995, and 10 years later more syntactically by Oury, has never given rise to an effective translation. In this paper, we provide the first syntactical translation from ETT to ITT with uniqueness of identity proofs and functional extensionality. This translation has been defined and proven correct in Coq and yields an executable plugin that translates a derivation in ETT into an actual Coq typing judgment. Additionally, we show how this result is extended in the context of homotopy to a two-level type theory.
| Titel: |
Eliminating Reflection from Type Theory ; Eliminating Reflection from Type Theory: To the Legacy of Martin Hofmann
|
|---|---|
| Autor/in / Beteiligte Person: | Winterhalter, Théo ; Sozeau, Matthieu ; Tabareau, Nicolas ; Gallinette : vers une nouvelle génération d'assistant à la preuve (LS2N - équipe 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) ; Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST) ; Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-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)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST) ; Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT) ; Design, study and implementation of languages for proofs and programs (PI.R2) ; Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)) ; Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) |
| Link: | |
| Zeitschrift: | CPP 2019 - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs ; https://hal.science/hal-01849166 ; CPP 2019 - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2019, Lisbonne, Portugal. pp.91-103, ⟨10.1145/3293880.3294095⟩ ; https://popl19.sigplan.org/track/CPP-2019, 2019 |
| Veröffentlichung: | HAL CCSD ; ACM, 2019 |
| Medientyp: | Konferenz |
| DOI: | 10.1145/3293880.3294095 |
| Schlagwort: |
|
| Sonstiges: |
|