Journal article
Game semantics for dependent types
- Abstract:
- We present a model of dependent type theory (DTT) with -, 1-, - and intensional Id-types, which is based on a slight variation of the (call-by-name) category of AJM-games and history-free winning well-bracketed strategies. The model satisfies Streicher’s criteria of intensionality and refutes function extensionality. The principle of uniqueness of identity proofs is satisfied. We show it contains a submodel as a full subcategory which gives a faithful interpretation of DTT with -, 1-, - and intensional Id-types and, additionally, finite inductive type families. This smaller model is fully (and faithfully) complete with respect to the syntax at the type hierarchy built without Id-types, as well as at the more general class of types where we allow for one strictly positive occurrence of an Id-type. Definability for the full type hierarchy with Id-types remains to be investigated.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Accepted manuscript, pdf, 610.8KB, Terms of use)
-
- Publisher copy:
- 10.1016/j.ic.2018.02.015
Authors
+ John Templeton Foundation
More from this funder
- Funding agency for:
- Abramsky, S
- Grant:
- FA9550-12-1-0136
+ Air Force Office of Scientific Research
More from this funder
- Funding agency for:
- Abramsky, S
- Grant:
- FA9550-12-1-0136
+ National Science Foundation
More from this funder
- Funding agency for:
- Jagadeesan, R
- Grant:
- CCF 0916741
+ Engineering and Physical Sciences Research Council
More from this funder
- Funding agency for:
- Vákár, M
- Abramsky, S
- Grant:
- FA9550-12-1-0136
- Publisher:
- Elsevier
- Journal:
- Information and Computation More from this journal
- Volume:
- 261
- Issue:
- Part 2
- Pages:
- 401-431
- Publication date:
- 2018-02-09
- Acceptance date:
- 2016-12-03
- DOI:
- EISSN:
-
1090-2651
- ISSN:
-
0890-5401
- Keywords:
- Pubs id:
-
pubs:830080
- UUID:
-
uuid:7ae51c14-9cc4-41f0-8a81-291f5e5682e4
- Local pid:
-
pubs:830080
- Source identifiers:
-
830080
- Deposit date:
-
2018-10-12
Terms of use
- Copyright holder:
- Elsevier
- Copyright date:
- 2018
- Notes:
- Copyright © 2018 Published by Elsevier Inc. This is the accepted manuscript version of the article. The final version is available online from Elsevier at: https://doi.org/10.1016/j.ic.2018.02.015
If you are the owner of this record, you can report an update to it here: Report update to this record