Setoid Type Theory—A Syntactic Translation

Altenkirch, Thorsten; Boulier, Simon; Kaposi, Ambrus; Tabereau, Nicolas

Abstract

We introduce setoid type theory, an intensional type theory with a proof-irrelevant universe of propositions and an equality type satisfying functional extensionality and propositional extensionality. We justify the rules of setoid type theory by a syntactic translation into a pure type theory with a universe of propositions. We develop the notion of a syntactic translation and relate it to model constructions.

Citation

Altenkirch, T., Boulier, S., Kaposi, A., & Tabereau, N. (2019, October). Setoid Type Theory—A Syntactic Translation. Presented at 13th International Conference on Mathematics of Program Construction (MPC 2019), Porto, Portugal

• Presentation Conference Type: Edited Proceedings
• Conference Name: 13th International Conference on Mathematics of Program Construction (MPC 2019)
• Start Date: Oct 7, 2019
• End Date: Oct 9, 2019
• Acceptance Date: Jun 14, 2019
• Online Publication Date: Oct 20, 2019
• Publication Date: Oct 20, 2019
• Deposit Date: Jan 24, 2020
• Publicly Available Date: Oct 21, 2020
• Publisher: Springer
• Pages: 155-196
• Series Title: Lecture Notes in Computer Science
• Series Number: 11825
• Series ISSN: 0302-9743
• Book Title: Mathematics of Program Construction: 13th International Conference, MPC 2019, Porto, Portugal, October 7–9, 2019, Proceedings
• ISBN: 9783030336356
• DOI: https://doi.org/10.1007/978-3-030-33636-3_7
• Public URL: https://nottingham-repository.worktribe.com/output/2634853
• Publisher URL: https://link.springer.com/chapter/10.1007/978-3-030-33636-3_7
• Additional Information: First Online: 20 October 2019; Conference Acronym: MPC; Conference Name: International Conference on Mathematics of Program Construction; Conference City: Porto; Conference Country: Portugal; Conference Year: 2019; Conference Start Date: 7 October 2019; Conference End Date: 9 October 2019; Conference Number: 13; Conference ID: mpc2019; Conference URL: https://www.cs.nott.ac.uk/~pszgmh/mpc19.html; Type: Single-blind; Conference Management System: EasyChair; Number of Submissions Sent for Review: 22; Number of Full Papers Accepted: 15; Number of Short Papers Accepted: 0; Acceptance Rate of Full Papers: 68% - The value is computed by the equation "Number of Full Papers Accepted / Number of Submissions Sent for Review * 100" and then rounded to a whole number.; Average Number of Reviews per Paper: 3; Average Number of Papers per Reviewer: 4; External Reviewers Involved: Yes