Formulas as Processes, Deadlock-Freedom as Choreographies

All publications

Formulas as Processes, Deadlock-Freedom as Choreographies

Matteo Acclavio, Giulia Manara, Fabrizio Montesi [2025].
In proceedings of ESOP (1) 2025, pp. 23-55.

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 computation-as-derivation paradigm extends the reach of logical methods for the study of concurrency, by bridging gaps between logic, the expressiveness of the π-calculus, and the expressiveness of choreographic languages.

Links

Additional notes

None

Cite (BibTeX)

Click to expand

@inproceedings{DBLP:conf/esop/AcclavioMM25,
  author       = {Matteo Acclavio and
                  Giulia Manara and
                  Fabrizio Montesi},
  editor       = {Viktor Vafeiadis},
  title        = {Formulas as Processes, Deadlock-Freedom as Choreographies},
  booktitle    = {Programming Languages and Systems - 34th European Symposium on Programming,
                  {ESOP} 2025, Held as Part of the International Joint Conferences on
                  Theory and Practice of Software, {ETAPS} 2025, Hamilton, ON, Canada,
                  May 3-8, 2025, Proceedings, Part {I}},
  series       = {Lecture Notes in Computer Science},
  volume       = {15694},
  pages        = {23--55},
  publisher    = {Springer},
  year         = {2025},
  url          = {https://doi.org/10.1007/978-3-031-91118-7\_2},
  doi          = {10.1007/978-3-031-91118-7\_2},
  timestamp    = {Mon, 19 May 2025 15:56:30 +0200},
  biburl       = {https://dblp.org/rec/conf/esop/AcclavioMM25.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

A PDF is available (possibly a preprint):