ICFP 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025
Wed 15 Oct 2025 11:40 - 12:05 at Orchid West - Concurrency Chair(s): Andrew K. Hirsch

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 \emph{choreography}, and then mechanically \emph{project} it into correct implementations of its participating processes. A choreography can be expressed as a $\lambda$-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 $\lambda$-calculi can have their operational semantics defined with just a few rules, existing models for \emph{choreographic} $\lambda$-calculi have \emph{dozens} of complex rules and \emph{no clear or agreed-upon evaluation strategy}.

We show that functional choreographic programming is simple. Beginning with the Chor$\lambda$ model from previous work, we strip away inessential features to produce a ``core'' model called $\lambda^\chi$. We discover that underneath Chor$\lambda$'s apparently ad-hoc semantics lies a close connection to non-strict $\lambda$-calculi; we call the resulting evaluation strategy \emph{semilenient}. Then, inspired by previous non-strict calculi, we develop a notion of \emph{choreographic evaluation contexts} and a special \emph{commute} rule to simplify and explain the unusual semantics of functional choreographic languages. The extra structure leads us to a presentation of $\lambda^\chi$ with just ten rules, and a discovery of three missing rules in previous presentations of Chor$\lambda$. 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.

Wed 15 Oct

Displayed time zone: Perth change

10:50 - 12:05
ConcurrencyICFP Papers at Orchid West
Chair(s): Andrew K. Hirsch University at Buffalo, SUNY
10:50
25m
Talk
Fusing Session-Typed Concurrent Programming into Functional Programming
ICFP Papers
Chuta Sano McGill University, Deepak Garg MPI-SWS, Ryan Kavanagh Université du Québec à Montréal, Brigitte Pientka McGill University, Bernardo Toninho Instituto Superior Técnico - University of Lisbon
DOI
11:15
25m
Talk
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
ICFP Papers
Kwing Hei Li Aarhus University, Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen New York University, Philipp G. Haselwarter Aarhus University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University
DOI Pre-print
11:40
25m
Talk
Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)
ICFP Papers
Dan Plyukhin University of Southern Denmark, Xueying Qin University of Southern Denmark, Fabrizio Montesi University of Southern Denmark
DOI Pre-print