Algebraic Effects Meet Hoare Logic in Cubical Agda
summary
Library formalises algebraic effects with equations in Cubical Agda using quotient types instead of setoids, provides a free model plus concrete models, and ships mechanised proofs and artifacts. It adds an effect-generic Hoare logic for partial correctness (demonic nondeterminism), ties Hoare triples to equational reasoning via an elimination principle, and proves a key M-theorem that turns Hoare proofs into program equalities. Examples include a token-stream parsing DSL with get/put/choice/fail and step-indexing for recursion; the mechanisation is complete and reusable.
AI-written summary · about
chapters (13)
- 0:00Algebraic effects & Hoare logic
- 1:29Beyond syntax formalization
- 3:40Semantics as computation
- 5:46Models & program verification
- 7:15First-order effects framework
- 9:00Parsing DSL example
- 11:33Equational logic reasoning
- 13:24Limitations of axioms
- 13:46Effect-generic Hoare logic
- 16:44Hoare logic & equational reasoning
- 18:11M theorem benefits
- 19:14Languages as languages
- 19:35Q&A on Cubical Agda
related talks
14mAdequacy for Algebraic Effects Revisited
17mHefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects
11mLocal algebraic effect theories
25mCubical Synthetic Homotopy Theory
01h 07mAn introduction to synthetic guarded domain theory with applications to probabilistic(…)
15mHandling Bidirectional Control Flow
16mA Hoare-Logic Style Refinement Types Formalisation
20mFully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logica