Setoid type theory - a syntactic translation - Archive ouverte HAL Access content directly
Conference Papers Year :

Setoid type theory - a syntactic translation

(1) , (2, 3) , (4) , (2, 3)
1
2
3
4

Abstract

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
Origin : Files produced by the author(s)
Loading...

Dates and versions

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

Identifiers

Cite

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⟩
261 View
1704 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More