Jim Laird - A fully abstract semantics of locally bound exceptions
I shall present a game semantics of locally bound `ML-style' exceptions. This is based on Hyland-Ong games, but in addition to relaxing the constraints which impose functional behaviour on strategies (as in games models of other computational effects such as continuations and references) a new feature is required; `control pointers' which track the flow of control. Full abstraction results can now be proved for games models of lambda-calculi including any combination of exceptions, continuations and references. Significantly, the richer structure of the model of exceptions entails that they cannot be expressed compositionally in terms of continuations and references.