We Know I Know You Know; Choreographic Programming With Multicast and Multiply Located Values
summary
A new choreographic language 𐤄λsmall adds multiply located values and multicast so a value can be located at many parties; typechecking now implies deadlock freedom (proofs include normal B simulation and Deadlock Freedom). A Haskell library, multicore, implements these ideas with census polymorphism for sets of participants and shows congruent computation where multiple parties compute the same result without select/merge overhead. Case studies and a working library demonstrate practicality and no extra communication cost for many patterns.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:07Multiply located values benefits
- 3:59Flexibility and conciseness
- 5:25Multicore Haskell implementation
- 6:48Knowledge of choice problem
- 8:13Multilocal multicast vs select merge
- 11:44Comparison with predicate transformers
- 13:07Communication efficiency
- 14:10Dead branches in Helm
- 16:45Q&A
related talks
20mEfficient, Portable, Census-Polymorphic Choreographic Programming
11mChoreographic Quick Changes: First-Class Location (Set) Polymorphism
22mTowards Lightweight and Efficient Choreographic Cloud Services
30mHasChor: Functional Choreographic Programming for All
41mProgramming Distributed Systems
19mChorCaml: Functional Choreographic Programming in OCaml
25mRelax! The Semilenient Core of Choreographic Programming (Functional Pearl)
43mMesh