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 pr...
Expand abstract
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Authors
Bibliographic Details
- Publisher:
- Association for Computing Machinery Publisher's website
- 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
Item Description
- Language:
- English
- Keywords:
- Pubs id:
-
935426
- Local pid:
- pubs:935426
- Deposit date:
- 2021-05-01
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
Metrics
If you are the owner of this record, you can report an update to it here: Report update to this record