Conference item icon

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


Access Document


Files:
Publisher copy:
10.1145/3209108.3209207

Authors


More by this author
Institution:
University of Oxford
Division:
College Only
Oxford college:
University College
Role:
Author
Publisher:
Association for Computing Machinery Publisher's website
Pages:
739-748
Host title:
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
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-09T00:00:00Z
Event end date:
2018-07-12T00:00:00Z
DOI:
ISSN:
1043-6871
ISBN:
9781450355834
Language:
English
Keywords:
Pubs id:
935426
Local pid:
pubs:935426
Deposit date:
2021-05-01

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP