Toward Verified Library-Level Choreographic Programming with Algebraic Effects
summary
Claims that algebraic effects give a lightweight, formalizable basis for library-level choreographies, and presents an Agda prototype that models choreography operations as effects and implements endpoint projection as effect handlers. The library encodes Comm plus announce and enclave effects (called Comm/announce/enclave effects), runs a distributed-double example, and keeps the core choreography engine under 100 lines. Ongoing work proves soundness and refines location-typed located values.
AI-written summary · about
chapters (8)
- 0:00Verified choreographic programming
- 1:27Algebraic effects for choreography
- 4:38Algebraic effects in OCaml
- 8:34Communication effects for choreography
- 11:21Distributed double program
- 13:49Conditionals in choreographies
- 16:44Future directions
- 18:11Q&A
related talks
14mTowards Cumulative Abstract Semantics via Handlers (Short Paper)
33mExtensible Effects: A Leaner Cake for Purely Functional Code
15mAbstract Interpretation of Temporal Safety Effects of Higher Order Programs
39mDesigning software with effects systems
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
01h 28mA Galilean revolution for computing
52mThink Abstractly, Work Concretely
01h 05mVerifying Infinitely Many Programs at Once