Logical Relations for Effect Capabilities
summary
A calculus of effect capabilities appears with an operational translation that generates runtime labels and labeled effects and captures continuations up to the nearest matching handler so handlers behave like delimited control. Two logical‑relation models are built: one uses an existential semantic effect (and a largest‑effect trick plus quantifier alternation) to scale to polymorphism and composition, the other exposes the connection to shift0/reset0. The framework proves nontrivial equivalences (reader implementations and a reader ≡ state‑without‑put example) and supports pairs, existentials, recursion.
AI-written summary · about
chapters (14)
- 0:00Effect capabilities motivation
- 1:47Reader effect in Fram
- 3:54State and handlers
- 7:57Label translation runtime
- 9:23Typing first-class handlers
- 10:27Logical relation foundations
- 12:33Handler types semantics
- 15:02Handler capabilities by labels
- 17:57Return and finally clauses
- 20:48Testing logical relations
- 21:10Reader vs state implementations
- 22:33Reader and state equivalence
- 24:21Key takeaways
- 25:47Q&A
related talks
25mA Relational Separation Logic for Effect Handlers
14mAdequacy for Algebraic Effects Revisited
30mEffects,capabilities,and boxes: from scope-based reasoning to type-based reasoning and back
55mRows and Capabilities as Modal Effects
15mEffects as Capabilities: Effect Handlers and Lightweight Effect Polymorphism
29mCoeffects for Sharing and Mutation
12mCompiling Effect Handlers in Capability-Passing Style
15mHandling Bidirectional Control Flow