Local algebraic effect theories
summary
Proposes tracking equational theories inside computation types so code can assume only the equations actually observed, not a single global theory. Claims this yields sound local reasoning, implements recursion, products, lists, subtyping, a denotational semantics and a Coq formalization, and an implementation on top of the f framework with bidirectional type inference. Notes handler correctness is undecidable so correctness proofs remain manual or in Coq, and shows examples where local theories allow optimisations and equivalences global theories forbid.
AI-written summary · about
chapters (8)
- 0:00Intro
- 0:33Reasoning about programs
- 4:26Using equations
- 4:56Examples
- 6:42Handler correctness
- 7:43Benefits and drawbacks
- 8:47What has been done
- 9:50Future work
related talks
14mAdequacy for Algebraic Effects Revisited
22mAlgebraic Effects Meet Hoare Logic in Cubical Agda
19mExtensible Metatheory Mechanization via Family Polymorphism
29mMechanized monadic equational reasoning for ML references
52mType Theory and its Meaning Explanations
27mAn Equations Tutorial
30mOperational game semantics for generative algebraic effects and handlers
22mA Calculus of Inductive Linear Constructions