Certifying Choreography Compilation
Lu\'is Cruz-Filipe, Fabrizio Montesi, Marco Peressotti

TL;DR
This paper introduces the first certified choreography compiler for a nontrivial language with recursion, ensuring correctness in translating global choreographies into local process behaviors.
Contribution
It provides the first verified compilation process for a complex choreographic language, bridging global and local paradigms with formal correctness guarantees.
Findings
First certified compiler for recursive choreographies
Formal proof of correctness for choreography compilation
Supports nontrivial choreographic language with recursion
Abstract
Choreographic programming is a paradigm for developing concurrent and distributed systems, where programs are choreographies that define, from a global viewpoint, the computations and interactions that communicating processes should enact. Choreography compilation translates choreographies into the local definitions of process behaviours, given as terms in a process calculus. Proving choreography compilation correct is challenging and error-prone, because it requires relating languages in different paradigms (global interactions vs local actions) and dealing with a combinatorial explosion of proof cases. We present the first certified program for choreography compilation for a nontrivial choreographic language supporting recursion.
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.
