Combining and Relating Control Effects and their Semantics

TL;DR

This paper explores game semantics models for programming languages with complex control features like exceptions and continuations, comparing explicit control pointers and monad-based approaches to understand their semantics and soundness.

Contribution

It introduces and compares two methodologies for modeling control effects in game semantics, enhancing understanding of their expressiveness and soundness.

Findings

Explicit control pointers facilitate full abstraction and control flow analysis.

Monadic composition provides a semantic correspondence for complex control effects.

Establishing soundness involves relating explicit models to monad semantics.

Abstract

Combining local exceptions and first class continuations leads to programs with complex control flow, as well as the possibility of expressing powerful constructs such as resumable exceptions. We describe and compare games models for a programming language which includes these features, as well as higher-order references. They are obtained by contrasting methodologies: by annotating sequences of moves with "control pointers" indicating where exceptions are thrown and caught, and by composing the exceptions and continuations monads. The former approach allows an explicit representation of control flow in games for exceptions, and hence a straightforward proof of definability (full abstraction) by factorization, as well as offering the possibility of a semantic approach to control flow analysis of exception-handling. However, establishing soundness of such a concrete and complex model is a non-trivial problem. It may be resolved by establishing a correspondence with the monad semantics, based on erasing explicit exception moves and replacing them with control pointers.