Operational game semantics for generative algebraic effects and handlers
summary
Claims a trace-based operational game semantics for a typed call-by-value λ-calculus with algebraic effects, handlers and dynamic effect instances (new creates fresh first-class instances). Builds an operational trace model where moves encode calls, returns and observable effect actions, introduces canonicalisation that removes non-observable forward moves, and proves that the relaxed trace equivalence is sound for contextual equivalence while conjecturing full abstraction (completeness remains work in progress).
AI-written summary · about
chapters (10)
- 0:00Introduction
- 2:13Algebraic effects overview
- 5:05Dynamic effect generation
- 7:37Language formal definition
- 10:33Contextual equivalence examples
- 14:03Fully abstract models
- 16:08Operational game semantics
- 23:11Soundness and full abstraction
- 23:52Conclusion
- 24:17Q&A
related talks
14mAdequacy for Algebraic Effects Revisited
15mEffect Handlers, Evidently
22mType-Safe Code Generation With Algebraic Effects and Handlers
11mLocal algebraic effect theories
17mHefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects
54mRevisiting the Evolution of Effects (Invited Talk)
15mHandling Bidirectional Control Flow
29mLogical Relations for Effect Capabilities