Choreographic Quick Changes: First-Class Location (Set) Polymorphism
Ashley Samuelson, Andrew K. Hirsch, Ethan Cecchetti

TL;DR
This paper introduces $eta_{QC}$, a typed choreographic language with first-class process names and polymorphism over types and locations, enhancing expressiveness and ensuring deadlock freedom.
Contribution
It presents $eta_{QC}$, the first choreographic language with first-class location polymorphism and formal verification, addressing limitations of existing languages.
Findings
Supports algebraic and recursive data types
Ensures deadlock freedom through formal verification
Enables dynamic computation of process locations
Abstract
Choreographic programming is a promising new paradigm for programming concurrent systems where a developer writes a single centralized program that compiles to individual programs for each node. Existing choreographic languages, however, lack critical features integral to modern systems, like the ability of one node to dynamically compute who should perform a computation and send that decision to others. This work addresses this gap with , the first typed choreographic language with \emph{first class process names} and polymorphism over both types and (sets of) locations. also improves expressive power over previous work by supporting algebraic and recursive data types as well as multiply-located values. We formalize and mechanically verify our results in Rocq, including the standard choreographic guarantee of deadlock freedom.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Distributed systems and fault tolerance
