Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
9657911 | Theoretical Computer Science | 2005 | 26 Pages |
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.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
J. Laird,