THORSTEN ALTENKIRCH THORSTEN.ALTENKIRCH@NOTTINGHAM.AC.UK
Professor of Computer Science
Setoid Type Theory—A Syntactic Translation
Altenkirch, Thorsten; Boulier, Simon; Kaposi, Ambrus; Tabereau, Nicolas
Authors
Simon Boulier
Ambrus Kaposi
Nicolas Tabereau
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). Setoid Type Theory—A Syntactic Translation. In Mathematics of Program Construction: 13th International Conference, MPC 2019, Porto, Portugal, October 7–9, 2019, Proceedings (155-196). https://doi.org/10.1007/978-3-030-33636-3_7
Conference Name | 13th International Conference on Mathematics of Program Construction (MPC 2019) |
---|---|
Conference Location | Porto, Portugal |
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 |
Files
Mpc2019
(440 Kb)
PDF
You might also like
Should Type Theory Replace Set Theory as the Foundation of Mathematics?
(2023)
Journal Article
Constructing a universe for the setoid model
(2021)
Conference Proceeding
Big Step Normalisation for Type Theory
(2020)
Journal Article
Naive Type Theory
(2019)
Book Chapter
Towards a cubical type theory without an interval
(2018)
Journal Article
Downloadable Citations
About Repository@Nottingham
Administrator e-mail: digital-library-support@nottingham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search