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

TL;DR

This paper presents a logical approach to analyzing deadlock-freedom in the { ho}-calculus, establishing a correspondence between sequent calculus derivations and process computations, and demonstrating how choreographies can represent deadlock-free processes.

Contribution

It introduces a processes-as-formulas interpretation for the { ho}-calculus, providing a logical characterization of deadlock-freedom and a completeness result linking processes and choreographies.

Findings

Logical characterization of deadlock-freedom for recursion- and race-free { ho}-calculus

Representation of deadlock-free { ho}-calculus processes by choreographies

Extension of logical methods to concurrency analysis

Abstract

We introduce a novel approach to studying properties of processes in the {\pi}-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 {\pi}-calculus. Our method provides a simple logical characterisation of deadlock-freedom for the recursion- and race-free fragment of the {\pi}-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 {\pi}-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 {\pi}-calculus, and the expressiveness of choreographic languages.