Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)
summary
Presents a trimmed formal core called λχ with just ten operational rules and a new semilenient evaluation strategy that mixes lenient (evaluate under binders) and per-process determinism. Builds choreographic evaluation contexts plus one commuting-into-answer rule to generate the common commuting conversions, discovers three missing rules in earlier Chorλ proofs, and sketches how the machinery simplifies the projection (bisimulation) proof and could be mechanized.
AI-written summary · about
chapters (13)
- 0:00Choreographic programming intro
- 1:45Why choreographic programming
- 3:09Adding locations to programs
- 5:17Choreographic semantics models
- 7:02Higher-order choreography problem
- 9:11Cleaning choreographic semantics
- 12:44Deterministic vs concurrent eval
- 14:28Semilenient evaluation intro
- 16:34Commuting conversions
- 18:41Simplifying rules with frames
- 20:47Semantics strict vs lenient
- 21:30Open questions future work
- 22:11Closing Q&A
related talks
20mEfficient, Portable, Census-Polymorphic Choreographic Programming
19mChorCaml: Functional Choreographic Programming in OCaml
30mHasChor: Functional Choreographic Programming for All
20mPirouette: Higher-Order Typed Functional Choreographies
22mTowards Lightweight and Efficient Choreographic Cloud Services
11mChoreographic Quick Changes: First-Class Location (Set) Polymorphism
36mKlor: Choreographic Programming in Clojure
20mChoral: Object-Oriented Choreographic Programming