Operational game semantics for generative algebraic effects and handlers

on YouTube ↗24m

" summary

Describes a typed call-by-value λ-calculus with first-class effect instances and dynamic generation plus a public/private disclosure discipline; builds an operational game semantics as a labeled-transition trace model where moves record question/return, effect parameter and continuation names; proves the refined canonical trace equivalence is sound: trace equivalence implies contextual equivalence; conjectures completeness and outlines a definability approach plus a rewriting/forward-move permutation to remove intensional distinctions.

AI-written summary · about

" chapters (9)

1. 0:00Introduction to algebraic effects
2. 2:16Language syntax and modularity
3. 5:34Dynamic generation of effects
4. 7:21Contextual equivalence examples
5. 9:50Operational game semantics
6. 12:22Labeled transition systems
7. 14:30Modeling observable effects
8. 18:14Results and conclusion
9. 20:25Questions and discussion