Game semantics for dependent types
- Submitting institution
-
University of Oxford
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 2051
- Type
- D - Journal article
- DOI
-
10.1016/j.ic.2018.02.015
- Title of journal
- INFORMATION AND COMPUTATION
- Article number
- -
- First page
- 401
- Volume
- 261
- Issue
- Part 2
- ISSN
- 0890-5401
- Open access status
- Not compliant
- Month of publication
- February
- Year of publication
- 2018
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
2
- Research group(s)
-
-
- Citation count
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Game semantics has had a major impact on the semantics of programming languages and its applications, as recognised by the announcement of the 2017 Alonzo Church award, of which Abramsky was one of the joint winners. This paper is the first successfully to extend game semantics to dependent types, a key feature of current advanced type theories for programming languages and proof systems. This is a major step towards getting a computationally meaningful semantics for homotopy type theory and related systems. The paper was selected from ICALP 2015 for the special issue in Information and Computation.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -