Linear Logic, the π-calculus, and their Metatheory: A Recipe for Proofs as Processes

Fabrizio Montesi, Marco Peressotti [2021].
In CoRR abs/2106.11818.

Abstract

Initiated by Abramsky [1994], the Proofs as Processes agenda is to establish a solid foundation for the study of concurrent languages, by researching the connection between linear logic and the $\pi$-calculus. To date, Proofs as Processes is still a partial success. Caires and Pfenning [2010] showed that linear propositions correspond to session types, which prescribe the observable behaviour of processes. Further, Carbone et al. [2018] demonstrated that adopting devices from hypersequents [Avron 1991] shapes proofs such that they correspond to the expected syntactic structure of processes in the $\pi$-calculus. What remains is reconstructing the expected metatheory of session types and the $\pi$-calculus. In particular, the hallmark of session types, session fidelity, still has to be reconstructed: a correspondence between the observable behaviours of processes and their session types, in terms of labelled transitions. In this article, we present $\pi$LL, a new process calculus rooted in linear logic. The key novelty of $\pi$LL is that it comes with a carefully formulated design recipe, based on a dialgebraic view of labelled transition systems. Thanks to our recipe, $\pi$LL offers the expected transition systems of session types, which we use to establish session fidelity. We use $\pi$LL to carry out the first thorough investigation of the metatheoretical properties enforced by linear logic on the observable behaviour of processes, uncovering connections with similarity and bisimilarity. We also prove that $\pi$LL and our recipe form a robust basis for the further exploration of Proofs as Processes, by considering different features: polymorphism, process mobility, and recursion.

Links

arxiv.org

Additional notes

None

Cite (BibTeX)

Click to expand

@article{DBLP:journals/corr/abs-2106-11818,
  author       = {Fabrizio Montesi and
                  Marco Peressotti},
  title        = {Linear Logic, the {\(\pi\)}-calculus, and their Metatheory: {A} Recipe
                  for Proofs as Processes},
  journal      = {CoRR},
  volume       = {abs/2106.11818},
  year         = {2021},
  url          = {https://arxiv.org/abs/2106.11818},
  eprinttype    = {arXiv},
  eprint       = {2106.11818},
  timestamp    = {Wed, 30 Jun 2021 16:14:10 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2106-11818.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}