Laird, James (2005) Game semantics and Linear CPS interpretation. Theoretical Computer Science, 333. pp. 199-224. ISSN 03043975
Full text not available from this repository.Abstract
We 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.
Item Type: | Article |
---|---|
Schools and Departments: | School of Engineering and Informatics > Informatics |
Depositing User: | James David Laird |
Date Deposited: | 06 Feb 2012 18:33 |
Last Modified: | 31 May 2012 10:59 |
URI: | http://sro.sussex.ac.uk/id/eprint/17088 |