Towards Lightweight and Efficient Choreographic Cloud Services
summary
Extensions to HasChor called CloudChor add concrete primitives: multiply-located values (a type-level list + np proxies), scatter/gather operators and a multilocally primitive, plus optimized branching via static analysis (enumeration of branch scrutinees) that reduces broadcast overhead. Formal semantics and proofs (soundness and completeness of endpoint projection, deadlock freedom via confluence) back the design. A data clean room protocol is implemented by lowering to Haskell primitives and runs end-to-end; prototypes exist but full production hardening (fault models, scaling) remains ongoing.
AI-written summary · about
chapters (9)
- 0:00Choreographic programming intro
- 2:28Hascore API in Haskell
- 6:46Hascore limits for protocols
- 7:28Multiplicated values in Cloud Core
- 10:39Data clean room protocols
- 11:42Optimizing choreography branches
- 15:53Formal semantics & deadlock freedom
- 16:36Conclusion & future work
- 17:28Q&A
related talks
30mHasChor: Functional Choreographic Programming for All
20mEfficient, Portable, Census-Polymorphic Choreographic Programming
19mChorCaml: Functional Choreographic Programming in OCaml
36mKlor: Choreographic Programming in Clojure
20mChoral: Object-Oriented Choreographic Programming
25mRelax! The Semilenient Core of Choreographic Programming (Functional Pearl)
19mWe Know I Know You Know; Choreographic Programming With Multicast and Multiply Located Values
11mChoreographic Quick Changes: First-Class Location (Set) Polymorphism