Setoid type theory - a syntactic translation

Thorsten Altenkirch 1 Simon Boulier 2, 3 Ambrus Kaposi 4 Nicolas Tabareau 2, 3
1 Functional Programming Laboratory
2 GALLINETTE - Gallinette : vers une nouvelle génération d'assistant à la preuve
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
3 LS2N - Laboratoire des Sciences du Numérique de Nantes
4 ELTE - Eötvös Loránd University
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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [34 references]  Display  Hide  Download
https://hal.inria.fr/hal-02281225
Contributor : Nicolas Tabareau <>
Submitted on : Sunday, September 8, 2019 - 11:55:23 PM
Last modification on : Wednesday, October 23, 2019 - 5:10:08 PM

File

mpc2019.pdf
Files produced by the author(s)

Identifiers

Collections

EC-NANTES | UNAM | CNRS | LS2N | INRIA | UNIV-NANTES | LS2N-GALLINETTE

Citation

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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

79

Files downloads

668

 

 

Contact

archive-ouverte@inria.fr