Certifying Choreography Compilation

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.