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 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.
- Full text (.pdf)<\li>
- Extended Abstract (.pdf) presented at FoSSaCS '03<\li>
- Bibtex entry:
@article{linlong,
author = "J. Laird",
title = "Game Semantics and {L}inear {CPS} Interpretation",
journal = "Theoretical Computer Science",
volume = "333",
pages = "199--224",
publisher = "Elsevier",
year = 2005}