Combining control effects and their models: Game semantics for a hierarchy of static, dynamic and delimited control effects

This paper develops operational and denotational semantics for a hierarchy of programming languages which include combinations of locally declared control prompts to which a program can escape, with first-class continuations which may either capture their enclosing prompts, or be delimited by them. We describe two different hierarchies of models, both based on categories of games and strategies with a computational monad, but obtained using different methodologies. By relaxing combinations of behavioural constraints on strategies with control flow represented by annotation with control pointers we are able to give direct and explicit characterizations of control operators and their effects, including examples characterizing their macro-expressiveness. By constructing a parallel hierarchy of models by applying sequences of monad transformers, and relating these to the direct interpretation of control effects, we obtain games interpretations of higher-level abstractions such as continuations and exceptions, which can be used as the basis for equational reasoning about programs.