CP 2026: Choreographic Programming
Basics
| Field | Value |
|---|---|
| Date | |
| Room | Trailhead |
| Parent | PLDI 2026, Boulder CO |
| Page | pldi26.sigplan.org/home/cp-2026 |
| Chairs | Andrew K. Hirsch (Buffalo), Dan Plyukhin (USD) |
| Recording | Trailhead — CP (Jun 16) |
What choreographic programming is
Write one global program – a choreography (Alice -> Bob: msg) – and a
compiler step, endpoint projection (EPP), generates the per-participant local
programs. The projected endpoints are deadlock-free and communication-safe by
construction: you cannot write a choreography that projects to a deadlock. The
lineage is multiparty session types (Honda/Yoshida) made executable; the
languages to know are Choral (Montesi, OO/Java) and HasChor (Kuper's group,
Haskell, library-level dynamic projection).
Program (Tue 16 Jun 2026, Trailhead)
| Time | Kind | Talk | Who |
|---|---|---|---|
| 09:10 | Keynote | Interpreters everywhere! | Lindsey Kuper (UCSC) |
| 10:40 | Applications | The Chor of the Message Passing Interface (MPI) | Allen, Hirsch (Buffalo) |
| 11:05 | Applications | Towards Quantum Choreographies | Paykin, Near, Skalka (Vermont) |
| 11:30 | Applications | Pact: A Choreographic Language for Agentic Ecosystems | Gopinathan, Feser, Naim, Tavares, Bingham (Basis) |
| 11:55 | Applications | Towards Choreographic Programming for Consensus Protocols | Zhang, Gancher (Northeastern) |
| 13:40 | Foundations | Probabilistic Performance of Asynchronous Data-Flow Choreographies | Bates (Vermont) |
| 14:05 | Foundations | Bushwhacking towards Event-Driven Chorex | Wiersdorf, Greenman (Utah) |
| 14:30 | Foundations | Formalizing Select-&-Merge ≡ Conclaves-&-MLVs | Bates, Qin, Near, Peressotti (Vermont/USD) |
| 14:55 | Foundations | Parametric Choreographies for Distributed Programming | Liagouris, Das (Boston U.) |
| 15:50 | Business | CP business meeting | chair: Plyukhin |
Keynote — Lindsey Kuper, "Interpreters everywhere!"
Framing from the Friedman/EOPL lineage: "my work is still about interpreters." Two lines from her group, each reduced to an interpreter question:
- Library-level choreographic programming – write a distributed program as a single unified program in your host language, then dynamically project it to endpoints. The question: what if endpoint projection were an interpreter? (this is the HasChor design – projection as an effect handler, not a compiler pass.)
- Causal separation diagrams – inductively-defined data structures for elegant mechanized reasoning about happens-before in concurrent executions. The question: what if you could write interpreters for sequence diagrams?
Connection to current research
The correct-by-construction leg
The Shan Lu PAgE keynote notes name a distributed-correctness trichotomy and leave one slot empty – "cross-reference correct-by-construction and Jepsen/Antithesis as the empirical-testing complement to mechanized proof." CP fills that third slot:
| Approach | Exemplar | What it does |
|---|---|---|
| Prove | Verus / Anvil / IronFleet | verify a distributed system you wrote |
| Test | Jepsen / Antithesis (BugBash) | inject faults, find violations |
| Construct | choreographies / EPP | make a deadlocking implementation impossible |
The sharp contrast: Verus verifies a system you wrote; a choreography makes you unable to write one that deadlocks. Same correctness axis, opposite end.
Pact, and choreographies for agents
Pact: A Choreographic Language for Agentic Ecosystems (Basis) is the talk that crosses into our agentic thread directly. Swap "participants" for "agents" and a choreography is a global multi-party spec that projects to deadlock-free endpoints – a correct-by-construction answer to how do orchestrated agents coordinate without deadlock, where the global protocol is the spec and each agent is a projected endpoint. The complement to PAgE's verify-the-agent's-output stance: here the coordination is correct before any agent runs.
Where it is orthogonal
This is protocol correctness across concurrent parties (deadlock-freedom, communication safety), not the data correctness of a sequential tool (One Tool, Four Ways – the round-trip law). Same "types buy guarantees" spirit, a different axis. And Kuper's "EPP as interpreter" framing rhymes with the repl-driven / interpreter thread.
Reading list
- Montesi & Carbone, Kickstarting Choreographic Programming – arXiv:1502.02519
- Shen, Kashiwa, Kuper, HasChor: Functional Choreographic Programming for All (functional pearl) – arXiv:2303.00924
- Giallorenzo et al., Choral: Object-Oriented Choreographic Programming – arXiv:2005.09520
- Real-World Choreographic Programming (full-duplex, interop) – arXiv:2303.03983
- Montesi, bliki entry – https://www.fabriziomontesi.com/bliki/ChoreographicProgramming
Related
- PLDI 2026 – parent conference
- PAgE 2026 – agentic-engineering workshop (verify-the-proof side); Shan Lu keynote
- BugBash 2026 – testing-side complement (Antithesis, DST)