A game semantics of linearly used continuations

Research output: Chapter in Book/Report/Conference proceedingChapter

7 Citations (Scopus)

Abstract

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
Pages313-327
Number of pages15
ISBN (Print)9783540008972
DOIs
Publication statusPublished - 2003

Publication series

NameLecture Notes in Computer Science
Volume2620

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

Cite this