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.

@article{paperbot3038,
  title = {Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)},
  author = {Dan Plyukhin and Xueying Qin and Fabrizio Montesi},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {ICFP},
  year = {2025},
  doi = {10.1145/3747538}
}