CP 2024: International Workshop on Choreographic Programming
Basics
| Field | Value |
|---|---|
| Event | International Workshop on Choreographic Programming (CP 2024) |
| Date | |
| Venue | Finland room, Radisson Blu Scandinavia, Copenhagen, Denmark |
| Co-located | PLDI 2024 (ACM SIGPLAN) |
| Page | pldi24.sigplan.org/home/cp-2024 |
| Organizers | Saverio Giallorenzo (Bologna / INRIA), Lindsey Kuper (UC Santa Cruz), Marco Peressotti (SDU) |
What choreographic programming is
You write the global protocol — one program describing what every role does and how they exchange messages — and the compiler projects it into the per-role local implementations. The choreography is the single source of truth, so whole classes of protocol bugs (deadlock from mismatched send/receive, drift between a spec and its implementations) become unrepresentable rather than tested-for.
The claim to interrogate is the strength of that "unrepresentable": what the projection actually guarantees, and what it silently assumes about the network. Two talks below attack exactly that (communication failures; information flow).
Keynote
Choreographic Programming: its essence, beauty, and necessity — Fabrizio Montesi (University of Southern Denmark), 09:10–10:10. Montesi wrote the field's standard treatment; this is the framing talk, not a results talk.
Program
Theory & Verification (10:40–12:20, chair: Giallorenzo)
| Time | Talk | Authors |
|---|---|---|
| 10:40 | A Propositional Dynamic Logic for Choreographies | Matteo Acclavio, Fabrizio Montesi, Marco Peressotti |
| 11:00 | Choreographic Programming in Modal Type Theory | Maxim Urschumzew, Miëtek Bak |
| 11:20 | Choreographies meet Communication Failures | Eva Graversen, Fabrizio Montesi, Marco Peressotti |
| 11:40 | Corps: A Core Calculus of Hierarchical Choreographic Programming | Andrew K. Hirsch (University at Buffalo, SUNY) |
| 12:00 | Masquerade: Information Flow Control for Choreographies | Michael Piskozub, Ethan Cecchetti, Andrew K. Hirsch |
Languages & Verification (13:40–15:20, chair: Kuper)
| Time | Talk | Authors |
|---|---|---|
| 13:40 | A Probabilistic Choreography Language for PRISM | Marco Carbone (IT University of Copenhagen), Adele Veschetti |
| 14:00 | A Function-as-a-Service Choreographic Programming Language: Examples and Applications | Giuseppe De Palma, Saverio Giallorenzo, Jacopo Mauro, Matteo Trentin, Gianluigi Zavattaro |
| 14:20 | Exploring Algebraic Placement in Multiparty Languages | George Zakhour, Pascal Weisenburger, Guido Salvaneschi (University of St. Gallen) |
| 14:40 | Poroutines: The Essence of Choreographic Programming? | Dan Plyukhin (SDU) |
| 15:00 | We Know I Know You Know; Choreographic Programming With Multicast and Multiply Located Values | Mako P. Bates, Joseph P. Near (University of Vermont) |
Libraries (16:00–17:20, chair: Peressotti)
| Time | Talk | Authors |
|---|---|---|
| 16:00 | ChoRus: Library-Level Choreographic Programming in Rust | Shun Kashiwa, Lindsey Kuper |
| 16:20 | Klor: Choreographies for the Working Clojurian | Lovro Lugović, Sung-Shik Jongmans |
| 16:40 | Suki: Choreographed Distributed Dataflow in Rust | Shadaj Laddad, Alvin Cheung, Joseph M. Hellerstein (UC Berkeley) |
| 17:00 | Toward Verified Library-Level Choreographic Programming with Algebraic Effects | Gan Shen, Lindsey Kuper (UC Santa Cruz) |
Opening 09:00, closing 17:20–17:40, informal dinner 18:30 at Broens Gadekøkken.
Why this workshop, backfilled two years later
Klor — the Clojure line
lovrosdu/klor (Lugović, Jongmans — SDU / Open University of the Netherlands)
is choreographic programming as a normal Clojure library: a DSL, not a new
language with its own toolchain. That is the interesting move — library-level
implementations trade some static guarantee for the ability to live inside an
existing ecosystem, and the whole Libraries session above is an argument about
where that trade lands. ChoRus and Suki make the same bet in Rust; Shen and
Kuper's algebraic-effects talk is the attempt to buy the guarantee back.
Klor was presented again three months later at Heart of Clojure 2024 (Sept, Leuven) — research workshop first, community talk second. Funded in part under NLnet's "Choreographic Programming: From Theory To Practice".
The Kuper thread
Lindsey Kuper co-organised this workshop and co-authored two of its talks. She is a keynote speaker at ICFP 2026 ("Interpreters everywhere!") — the same distributed-systems-meets-PL territory, two years on.
Related notes crosslink
- Clojure side
- Heart of Clojure 2024 (the Klor community talk).
- SIGPLAN neighbours
- PLDI 2026 (the parent conference, two editions later) · ICFP 2026 · POPL 2026.
- Formal-methods adjacency
- TLA+ for system design — the specify-the-protocol- globally instinct, without the compiler doing the projection.
- Category-theoretic framing
- category theory in computing.
Claims to test refutation
- Projection from a choreography eliminates deadlock by construction
- a projected system that deadlocks anyway — which is precisely what "Choreographies meet Communication Failures" is about, so read that talk before repeating the claim unqualified.
- (no term)
- Library-level choreographies (Klor, ChoRus, Suki) give up nothing important versus a dedicated choreographic language :: a protocol expressible in a standalone choreographic language whose projection the library cannot check, pushing the error to runtime.
- The choreography stays the single source of truth
- any deployment where a role's local implementation is hand-edited after projection.
- (no term)
Follow-up
[ ]Read Montesi's keynote framing against the Klor tutorial (tutorial-01-introduction)[ ]Try Klor on a small two-role protocol; see what the projection rejects[ ]Check whether CP has run again since 2024 and where it co-located[ ]"Choreographies meet Communication Failures" — what failure model, and does it cover partition rather than just message loss