Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)

Dan Plyukhin, Xueying Qin, Fabrizio Montesi [2025].
In Proc. ACM Program. Lang. 9.

Abstract

The past few years have seen a surge of interest in choreographic programming, a programming paradigm for concurrent and distributed systems. The paradigm allows programmers to implement a distributed interaction protocol with a single high-level program, called a choreography , and then mechanically project it into correct implementations of its participating processes. A choreography can be expressed as a λ-term parameterized by constructors for creating data “at” a process and for communicating data between processes. Through this lens, recent work has shown how one can add choreographies to mainstream languages like Java, or even embed choreographies as a DSL in languages like Haskell and Rust. These new choreographic languages allow programmers to write in applicative style (like in functional programming) and write higher-order choreographies for better modularity. But the semantics of functional choreographic languages is not well-understood. Whereas typical λ-calculi can have their operational semantics defined with just a few rules, existing models for choreographic λ-calculi have dozens of complex rules and no clear or agreed-upon evaluation strategy . We show that functional choreographic programming is simple. Beginning with the Chorλ model from previous work, we strip away inessential features to produce a “core” model called λ χ . We discover that underneath Chorλ’s apparently ad-hoc semantics lies a close connection to non-strict λ-calculi; we call the resulting evaluation strategy semilenient . Then, inspired by previous non-strict calculi, we develop a notion of choreographic evaluation contexts and a special commute rule to simplify and explain the unusual semantics of functional choreographic languages. The extra structure leads us to a presentation of λ χ with just ten rules, and a discovery of three missing rules in previous presentations of Chorλ. We also show how the extra structure comes with nice properties, which we use to simplify the correspondence proof between choreographies and their projections. Our model serves as both a principled foundation for functional choreographic languages and a good entry point for newcomers.

Links

doi.org

Additional notes

None

Cite (BibTeX)

Click to expand

@article{DBLP:journals/pacmpl/PlyukhinQM25,
  author       = {Dan Plyukhin and
                  Xueying Qin and
                  Fabrizio Montesi},
  title        = {Relax! The Semilenient Core of Choreographic Programming (Functional
                  Pearl)},
  journal      = {Proc. {ACM} Program. Lang.},
  volume       = {9},
  number       = {{ICFP}},
  pages        = {947--973},
  year         = {2025},
  url          = {https://doi.org/10.1145/3747538},
  doi          = {10.1145/3747538},
  timestamp    = {Wed, 25 Feb 2026 08:22:19 +0100},
  biburl       = {https://dblp.org/rec/journals/pacmpl/PlyukhinQM25.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}