Operational Game Semantics for Generative Algebraic Effects and Handlers

Explore an ongoing research project focused on developing a fully abstract trace semantics for a typed call-by-value λ-calculus with algebraic effects and handlers in this 24-minute conference talk presented at GALOP'24. Delve into the innovative approach of using an operational presentation of game semantics to build a trace model that represents the interaction between programs and their environments. Learn about the language's unique feature of dynamic allocation of effect instances, which are treated as first-class values and can be exchanged. Gain insights into the challenges and potential applications of this work in the field of programming language semantics and effect systems.

[GALOP'24] Operational game semantics for generative algebraic effects and handlers