Choreographic Quick Changes: First-Class Location (Set) Polymorphism
summary
A new choreographic language, λQC, adds first-class process names and polymorphism over types and sets of locations, plus algebraic and recursive data types and multiply-located values. It compiles via endpoint projection and mechanically verifies deadlock freedom and other guarantees in Rocq. The implementation paper includes reproducible artifacts (Zenodo) and claims this design lets a node dynamically compute and send who should act without introducing dependent types or losing type safety.
AI-written summary · about
chapters (9)
- 0:00Choreographic programming intro
- 1:26Choreographies simplify concurrency
- 2:30Alice buying a book example
- 3:53Dynamic process selection problems
- 6:19First-class process names solution
- 7:22Implementing the solution challenges
- 9:51Avoiding dependent types
- 10:34Knowledge of choice problem solved
- 10:55Choreographic quick change summary
related talks
20mEfficient, Portable, Census-Polymorphic Choreographic Programming
19mChorCaml: Functional Choreographic Programming in OCaml
19mWe Know I Know You Know; Choreographic Programming With Multicast and Multiply Located Values
22mTowards Lightweight and Efficient Choreographic Cloud Services
25mRelax! The Semilenient Core of Choreographic Programming (Functional Pearl)
20mPirouette: Higher-Order Typed Functional Choreographies
20mChoral: Object-Oriented Choreographic Programming
36mKlor: Choreographic Programming in Clojure