Efficient, Portable, Census-Polymorphic Choreographic Programming
summary
Claims that conclaves and multiply-located values remove redundant broadcasts and make conditionals communication-efficient, with a formal lambda-C showing preservation, progress, and sound endpoint projection. Introduces census polymorphism to write one choreography for variable numbers of participants (authors cite deployments with thousands), and provides library implementations—Haskell, Rust, TypeScript—with reusable artifacts and case studies; endpoint projection is implemented via dependency-injection interfaces and the prototypes compile and run.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 1:04Why choreographic programming matters
- 3:54Existing systems and limits
- 4:59Managing choice in choreographies
- 6:02Introducing censuses and conclaves
- 7:50Multiply values and efficient comms
- 9:33Formal properties of lambda C
- 10:15Implementation strategies
- 11:58Library-level benefits
- 13:01Census polymorphism in protocols
- 14:25Library design and helpers
- 15:49Adapting across languages
- 16:30Summary and implementations
- 17:35Q&A
related talks
19mWe Know I Know You Know; Choreographic Programming With Multicast and Multiply Located Values
19mChorCaml: Functional Choreographic Programming in OCaml
30mHasChor: Functional Choreographic Programming for All
22mTowards Lightweight and Efficient Choreographic Cloud Services
11mChoreographic Quick Changes: First-Class Location (Set) Polymorphism
25mRelax! The Semilenient Core of Choreographic Programming (Functional Pearl)
20mPirouette: Higher-Order Typed Functional Choreographies
20mChoral: Object-Oriented Choreographic Programming