Setoid type theory - a syntactic translation - Ecole Centrale de Nantes Accéder directement au contenu
Communication Dans Un Congrès Année : 2019

Setoid type theory - a syntactic translation

Résumé

We introduce setoid type theory, an intensional type theory with a proof-irrelevant universe of propositions and an equality type satisfying function extensionality, propositional extensionality and a definitional computation rule for transport. We justify the rules of setoid type theory by a syntactic translation into a pure type theory with a universe of propositions. We conjecture that our syntax is complete with regards to this translation.
Fichier principal
Vignette du fichier
mpc2019.pdf (429.81 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02281225 , version 1 (08-09-2019)

Identifiants

Citer

Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau. Setoid type theory - a syntactic translation. MPC 2019 - 13th International Conference on Mathematics of Program Construction, Oct 2019, Porto, Portugal. pp.155-196, ⟨10.1007/978-3-030-33636-3_7⟩. ⟨hal-02281225⟩
322 Consultations
2087 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More