Choreographic Programming

← Back to Home

Write a whole distributed system as one script, and let the compiler split it up.

A distributed system is normally written as many separate programs, one per participant, which have to agree on a protocol that exists nowhere in the code. Choreographic programming writes the interaction once, as a single program that names every participant, and a compiler projects it onto the individual endpoints. Protocol mismatches and whole classes of deadlock become programs you cannot write in the first place.

  • Foundations: how choreographic and multitier languages relate (ECOOP'21).
  • Applications: enforcing contract-client protocols in decentralized apps (TOPLAS'23).
  • Mechanized metatheory in Lean, with Timon Böhler and Simon Daniel: choreographies without variable binding, without “impossible” branches, and with deadlock freedom independent of the compiler (TyDe'26, preprint).
Highlight
  • 🏅 Distinguished Paper Multiparty Languages: the Choreographic and Multitier Cases, ECOOP 2021
Collaborators
Timon Böhler Jonathan I. Brachthäuser Simon Daniel Sebastian Faust Saverio Giallorenzo David Kretzler Mira Mezini Fabrizio Montesi Marius Müller Marco Peressotti Guido Salvaneschi Phillip Schuster Pascal Weisenburger

Timeline

2021ECOOP · Pearl

Multiparty Languages: the Choreographic and Multitier Cases

Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, David Richter, Guido Salvaneschi, Pascal Weisenburger

Choreographic and multitier languages grew out of different theories (process calculi vs. lambda calculus) in two communities with little contact. We show they differ in exactly two respects, perspective (objective vs. subjective) and whether communication is written down or implied, and give translations in both directions between minimal versions of each, so results can carry over.

A choreographic program: an objective description of n roles, listing 'A computes X', 'A sends X to B', 'B computes Y' and so on
The equivalent multitier program: nested subjective descriptions by n peers, where A says 'I compute X', B says 'I take X', and so on

Fig. 1/2 from the paper.

Links: ECOOP 2021 · paper · video 🏅 Distinguished Paper

2023TOPLAS · ECOOP 2022

Prisma: A Tierless Language for Contract-Client Protocols

David Richter, David Kretzler, Pascal Weisenburger, Guido Salvaneschi, Sebastian Faust, Mira Mezini

In a decentralized app, contract and client are separate programs, so their protocol is only a convention, and a client that acts out of order can drive the contract off-protocol. Prisma writes both as one program and compiles it into a smart contract plus client, with a proof that no attacker-controlled client can force the contract off the source-level control flow.

Links: TOPLAS 2023 · ECOOP 2022 · extended abstract · artifact · github · arxiv

2026TyDe @ FPW Paris

Mechanizing Choreographic Programs and Hoare Logic

Timon Böhler, Simon Daniel, David Richter, Pascal Weisenburger, Mira Mezini

In machine-checked proofs about choreographies, variable binding and substitution usually dominate the effort. Modelling “receive a message” as a state transformer on the participant’s local state removes the binder altogether, yielding a Lean mechanization of sound and complete endpoint projection, deadlock freedom, confluence, and a Hoare logic for choreographies.

Links: arxiv

2026TyDe @ FPW Paris

On Eliminating the Impossible with Dependent Types

Simon Daniel, Timon Böhler, David Richter, Pascal Weisenburger, Mira Mezini

Embedded choreographic libraries model a value that a role may or may not own as an option type, so unwrapping it always leaves a dead “impossible” branch. In Lean, ownership becomes a machine-checked proof carried in the value’s type, giving a library with no error/undefined in its core, without losing expressivity relative to prior, partial libraries.

Links: arxiv

2026Unpublished draft (click to expand)

Choreographies First, Session Types Later

Phillip Schuster, David Richter, Marius Müller, Jonathan I. Brachthäuser, Mira Mezini

Classically, deadlock freedom of a choreography is proved for one specific compiler, so hand-editing a generated process voids the guarantee. Inferring a global type from the choreography and projecting one local type per role moves the proof onto the types: any process checked against its local type keeps the system deadlock-free, whether it was generated or written by hand.

(a) Choreographic programming: a choreography is projected directly to a process
(b) This paper: a choreography yields both a process and a global type, and the global type projects to a local type that the process satisfies
(c) Multiparty session types: a global type projects to a local type, which a hand-written process must satisfy

Fig. 1 from the paper.

Links: preprint

Open questions

Directions that come out of the work above, from thesis-sized (BSc/MSc) to PhD-scale:

  • Finer-grained choice. The Lean mechanization broadcasts every choice to the whole network. Supporting knowledge of choice, multiply-located values or enclaves would bring it closer to practical choreographic languages.
  • Realistic communication. Asynchronous messages, failures, and roles created at run time, while keeping global types inferable.
  • Composition. Assembling larger systems from independently verified choreographies and protocols.
  • Tooling. Making inferred global and local types useful to programmers, e.g. as protocol documentation or as a guide for safe refactoring.

Useful background is functional programming and some Lean or Scala; my Type Systems lecture covers the foundations. If one of these interests you, write me an email.