Functional Choreographic Programming
Lu\'is Cruz-Filipe, Eva Graversen, Lovro Lugovi\'c, Fabrizio Montesi,, Marco Peressotti

TL;DR
Chorλ is a novel functional choreographic programming language based on λ-calculus, providing a theoretical foundation for higher-order choreographies and bridging functional and choreographic programming communities.
Contribution
It introduces the first formal theory for higher-order choreographic programming using a λ-calculus framework, including new evaluation and typing strategies for distributed computation.
Findings
Supports higher-order choreographies with theoretical guarantees
Demonstrates expressivity through key examples from Choral
Bridges the gap between functional and choreographic programming communities
Abstract
Choreographic programming is an emerging programming paradigm for concurrent and distributed systems, whereby developers write the communications that should be enacted and then a distributed implementation is automatically obtained by means of a compiler. Theories of choreographic programming typically come with strong theoretical guarantees about the compilation process, most notably: the generated implementations operationally correspond to their source choreographies and are deadlock-free. Currently, the most advanced incarnation of the paradigm is Choral, an object-oriented choreographic programming language that targets Java. Choral deviated significantly from known theories of choreographies, and introduced the possibility of expressing higher-order choreographies (choreographies parameterised over choreographies) that are fully distributed. As a consequence, it is unclear if…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
