Journal article icon

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 i...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed

Actions


Access Document


Files:
Publisher copy:
10.1016/j.ic.2018.02.015

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS Division
Department:
Computer Science
Role:
Author
More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Oxford college:
Wolfson College
Role:
Author
ORCID:
0000-0003-3921-6637
More from this funder
Funding agency for:
Vákár, M
More from this funder
Funding agency for:
Jagadeesan, R
Grant:
CCF 0916741
More from this funder
Funding agency for:
Abramsky, S
Grant:
FA9550-12-1-0136
More from this funder
Funding agency for:
Abramsky, S
Grant:
FA9550-12-1-0136
Expand funders...
Publisher:
Elsevier Publisher's website
Journal:
Information and Computation Journal website
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
Source identifiers:
830080
Keywords:
Pubs id:
pubs:830080
UUID:
uuid:7ae51c14-9cc4-41f0-8a81-291f5e5682e4
Local pid:
pubs:830080
Deposit date:
2018-10-12

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