A game semantics of linearly used continuations

Research output: Chapter or section in a book/report/conference proceedingChapter or section

7 Citations (SciVal)


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.

Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures
Subtitle of host publicationProceedings 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
EditorsA. D. Gordon
Place of PublicationBerlin, Germany
PublisherSpringer Verlag
Number of pages15
ISBN (Print)9783540008972
Publication statusPublished - 2003

Publication series

NameLecture Notes in Computer Science


Dive into the research topics of 'A game semantics of linearly used continuations'. Together they form a unique fingerprint.

Cite this