Adequacy for Algebraic Effects Revisited
summary
Proves an adequacy theorem that covers a wide class of algebraic effects including infinitary cases, showing that denotational equality in a Call-by-Push-Value CBPV-style calculus implies observational equivalence. Uses operational semantics given by interaction trees and a denotational semantics via monad algebras, and gives a direct logical-relations proof generalizing Plotkin–Power’s finite result. Provides axioms for relational liftings, points out common liftings that fail the axioms, and sketches extensions toward recursive types without step indexing.
AI-written summary · about
chapters (7)
- 0:00Algebraic effects intro
- 2:10Revisiting adequacy
- 3:34Effects as system calls
- 6:23Denotational semantics
- 8:48Logical relations proof
- 10:32Recursive types challenges
- 12:07Q&A
related talks
22mAlgebraic Effects Meet Hoare Logic in Cubical Agda
11mLocal algebraic effect theories
29mLogical Relations for Effect Capabilities
15mStable Relations and Abstract Interpretation of Higher-Order Programs
26mObservational Equality: Now for Good
17mHefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects
30mOperational game semantics for generative algebraic effects and handlers
24mClassical Notions of Computation and the Hasegawa-Thielecke Theorem