We present an 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 abstract model of an affine type-theory - and a syntax-independent and full embedding of a category of HO-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 the call-by-value (untyped) λ-calculus, yielding a proof of full abstraction for the associated translation.
|Title of host publication||Foundations of Software Science and Computation Structures|
|Subtitle of host publication||Proceedings of 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003 Warsaw, Poland, April 7–11, 2003|
|Editors||A. D. Gordon|
|Place of Publication||Berlin, Germany|
|Number of pages||15|
|Publication status||Published - 2003|
|Name||Lecture Notes in Computer Science|