Operational Game Semantics for Generative Algebraic Effects and Handlers

Overview & Synopsis

We present a sound operational game semantics model (w.r.t. contextual equivalence) of a typed language with algebraic effects and handlers and dynamic generation of effect instances à la [5, 11]. We exhibit the interactive aspect of effect propagation, and to address it precisely, we identify the adequate granularity of the operational semantics (akin to [15]) and the decomposition of normal forms into their interactive and their observational part. To account for this additional form of interaction, we extend the standard pure interaction interface of game semantics consisting of questions and answers with effectful moves that involve the propagation of effects and the yielding of delimited continuations. Finally, we extend the well-bracketed constraint on the behavior of the environment, from the use of continuations as is standard in game semantics, to fragments of captured delimited continuations.