Pirouette: Higher-Order Typed Functional Choreographies
summary
Pirouette is a choreographic language that compiles a single higher-order functional program into one program per node via endpoint projection, with two function kinds (global and local) so functions may contain communication and closure-like captures as local values. Semantics use labeled steps plus a blocked-location set to permit safe out-of-order execution; merging makes projection partial and introduces a less-nondeterminism order. The design lifts any local message type system, proves progress/preservation, equivalence-typing, EPP soundness/completeness, and deadlock freedom by construction, and all results are Coq-verified.
AI-written summary · about
chapters (16)
- 0:00Intro
- 0:30Example
- 1:09deadlock
- 2:34previous solutions
- 3:25Pirouette
- 3:49Threaded Computation
- 4:36Global Types
- 5:25Local Data
- 7:43Two Types of Functions
- 8:27Summary
- 9:45Semantics
- 10:36Equivalence
- 12:00Evaluation
- 14:32Merging
- 15:45Theorems
- 16:58Conclusion
related talks
19mChorCaml: Functional Choreographic Programming in OCaml
20mEfficient, Portable, Census-Polymorphic Choreographic Programming
25mRelax! The Semilenient Core of Choreographic Programming (Functional Pearl)
30mHasChor: Functional Choreographic Programming for All
11mChoreographic Quick Changes: First-Class Location (Set) Polymorphism
36mKlor: Choreographic Programming in Clojure
14mMultiparty Motion Coordination: From Choreographies to Robotics Programs
20mChoral: Object-Oriented Choreographic Programming