Formulas as Processes, Deadlock-Freedom as Choreographies (Extended Version)

TL;DR

The paper develops a computation-as-deduction framework that models recursion-free $\pi$-calculus processes as formulas in a non-commutative linear logic, $\mathsf{PiL}$, linking operational reductions to linear implications. It proves that deadlock-freedom and progress correspond to derivability in $\mathsf{PiL}$ and achieves a strong completeness result showing that every race-free, deadlock-free finite network composed in parallel at the top level has a faithful choreography representation. By introducing choreographies, an endpoint projection mechanism, and a sequent calculus $\mathsf{ChorL}$ for the endpoint calculus, the authors establish a proofs-as-choreographies correspondence that characterizes the expressive power of choreographic programming in this setting. This work bridges logic, π-calculus expressiveness, and choreographic languages, enabling precise reasoning about cyclic dependencies, mobility, and safe coordination in concurrent systems.

Abstract

We introduce a novel approach to studying properties of processes in the π-calculus based on a processes-as-formulas interpretation, by establishing a correspondence between specific sequent calculus derivations and computation trees in the reduction semantics of the recursion-free π-calculus. Our method provides a simple logical characterisation of deadlock-freedom for the recursion- and race-free fragment of the π-calculus, supporting key features such as cyclic dependencies and an independence of the name restriction and parallel operators. Based on this technique, we establish a strong completeness result for a nontrivial choreographic language: all deadlock-free and race-free finite π-calculus processes composed in parallel at the top level can be faithfully represented by a choreography. With these results, we show how the paradigm of computation-as-derivation extends the reach of logical methods for the study of concurrency, by bridging important gaps between logic, the expressiveness of the π-calculus, and the expressiveness of choreographic languages.

Figures (17)

• Figure 1: Road map of the main technical results in this work.
• Figure 2: Formulas (with $x,y\in \mathcal{V}$), and their syntactic equivalences.
• Figure 3: Sequent calculus rules, with $\dagger\coloneqq x\notin \mathsf{free}(\Gamma)$.
• Figure 4: Syntax for $\pi$-calculus processes with $x,y\in\mathcal{N}$ and $L \subset\mathcal{L}$, and their sets of free and bound names.
• Figure 5: The standard $\alpha$-equivalence, and relations generating of the structural equivalence ($\equiv$) $\pi$-calculus processes, where $A{\Lleftarrow\!\!\!\!\!\Rrightarrow} B$ stands for $A\Rrightarrow B$ and $B\Rrightarrow A$.

Theorems & Definitions (53)

• remark 1
• theorem 1: acc:man:NL
• proposition 1: acc:man:NL
• theorem 2
• proof
• remark 2
• remark 3
• remark 4
• remark 5
• remark 6