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}