2025/01/15 by Matteo Acclavio, Acclavio, Matteo, Giulia Manara +3 · 1 citation
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2501.08928
openalex publication_date 2025/01/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/30
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.