File(s) not publicly available
Game semantics and Linear CPS interpretation
journal contribution
posted on 2023-06-07, 20:30 authored by James LairdWe present a semantic analysis of the “linearly used continuation-passing interpretation” of functional languages, based on game semantics. This consists of a category of games with a coherence condition on moves—yielding a fully complete model of an affine-type theory—and a syntax-independent and full embedding of a category of Hyland–Ong/Nickau-style “well-bracketed” games into it. We show that this embedding corresponds precisely to linear CPS interpretation in its action on a games model of call-by-value PCF, yielding a proof of full abstraction for the associated translation. We discuss extensions of the semantics to deal with recursive types, call-by-name evaluation, non-local jumps, and state.
History
Publication status
- Published
Journal
Theoretical Computer ScienceISSN
03043975Publisher
ElsevierExternal DOI
Volume
333Page range
199-224Pages
26.0Department affiliated with
- Informatics Publications
Full text available
- No
Peer reviewed?
- Yes
Legacy Posted Date
2012-02-06Usage metrics
Categories
No categories selectedKeywords
Licence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC