Conference item
Dialectica models of type theory
- Abstract:
- We present two Dialectica-like constructions for models of intensional Martin-Löf type theory based on Gödel's original Dialectica interpretation and the Diller-Nahm variant, bringing dependent types to categorical proof theory. We set both constructions within a logical predicates style theory for display map categories where we show that 'quasifibred' versions of dependent products and universes suffice to construct their standard counterparts. To support the logic required for dependent products in the first construction, we propose a new semantic notion of finite sum for dependent types, generalizing finitely-complete extensive categories. The second avoids extensivity assumptions using biproducts in a Kleisli category for a fibred additive monad.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Accepted manuscript, pdf, 731.9KB, Terms of use)
-
- Publisher copy:
- 10.1145/3209108.3209207
Authors
- Publisher:
- Association for Computing Machinery
- Host title:
- LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
- Pages:
- 739-748
- Publication date:
- 2018-07-09
- Acceptance date:
- 2018-03-31
- Event title:
- 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
- Event location:
- Oxford, UK
- Event website:
- https://lics.siglog.org/lics18/
- Event start date:
- 2018-07-09
- Event end date:
- 2018-07-12
- DOI:
- ISSN:
-
1043-6871
- ISBN:
- 9781450355834
- Language:
-
English
- Keywords:
- Pubs id:
-
935426
- Local pid:
-
pubs:935426
- Deposit date:
-
2021-05-01
- ARK identifier:
Terms of use
- Copyright holder:
- Sean K. Moss and Tamara von Glehn
- Copyright date:
- 2018
- Rights statement:
- © 2018 Copyright held by the owner/author(s). Publication rights licensed to the Association for Computing Machinery.
- Notes:
- This paper was presented at the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 9-12 July 2018, Oxford, UK. This is the accepted manuscript version of the paper. The final version is available online from the Association for Computing Machinery at: https://doi.org/10.1145/3209108.3209207
If you are the owner of this record, you can report an update to it here: Report update to this record