Abstract

We present games models of call-by-value functional-imperative languages with first-class continuations, and with (locally bound) exceptions, and give full abstraction results (using \emph{factorizations}) for these models. We show that continuations can be modelled by simply relaxing the bracketing condition on Hyland-Ong style games, exceptions require a new kind of ``contingency pointer'' to be added to sequences to ``track the flow of control'' and determine the dynamic binding of exceptions.

Using these results, we compare the expressive power of exceptions and continuations in a setting show that, contrary to ``folklore'', exceptions cannot be expressed using continuations and references, by comparing fully abstract models and extracting examples of contextual equivalences and other logical properties which are broken by exceptions, but not by continuations.

  • Extended abstract (.pdf)
  • Slides (.pdf) from the presentation at LICS '01.
  • Extended abstract (.pdf) of a related paper, using contexts derived from the semantics to show that exceptions cannot be macro-expressed by continuations and references (presented at ESOP '02).
  • Bibtex entry
    @Inproceedings{LLi,
    author = "J. Laird",
    title = "A fully abstract game semantics of local exceptions",
    booktitle = "Proceedings of LICS '01",
    publisher = "IEEE Computer Society Press",
    pages = "105--114",
    year = 2001}