Game semantics for interface middleweight Java
- Submitting institution
-
University of Oxford
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 15925
- Type
- D - Journal article
- DOI
-
10.1145/3428676
- Title of journal
- Journal of the ACM
- Article number
- 4
- First page
- 1
- Volume
- 68
- Issue
- 1
- ISSN
- 0004-5411
- Open access status
- Compliant
- Month of publication
- December
- Year of publication
- 2020
- 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
-
1
- Research group(s)
-
-
- Citation count
- 0
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- The quest for fully abstract models has been the driving force of denotational semantics. This paper uses game semantics to give the first denotational model of an object-oriented language that achieves full abstraction. The result, originally presented at POPL, was a flagship objective of the EPSRC-funded project “Game Semantics of Java Programs” (EP/J019577/1). The model was subsequently applied to verification tasks, inspiring new developments in automata theory over infinite alphabets (LICS'15 - https://doi.org/10.1109/LICS.2015.24; JCSS'17 - https://doi.org/10.1016/j.jcss.2017.02.008; ATVA'19 - https://doi.org/10.1007/978-3-030-31784-3), and leading to a classification of decidable cases for termination and equivalence, and a new verification tool Coneqct (both at ATVA'15).
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -