Proofs as Execution Trees for the π-Calculus

TL;DR

This paper defines a cut-free sequent calculus for an extension of first-order multiplicative and additive linear logic that includes a non-commutative and non-associative connective to faithfully model the prefix operator, and nominal quantifiers to represent name restriction.

Abstract

In this paper, we establish the foundations of a novel logical framework for the π-calculus, based on the deduction-as-computation paradigm. Following the standard proof-theoretic interpretation of logic programming, we represent processes as formulas, and we interpret proofs as computations. For this purpose, we define a cut-free sequent calculus for an extension of first-order multiplicative and additive linear logic. This extension includes a non-commutative and non-associative connective to faithfully model the prefix operator, and nominal quantifiers to represent name restriction. Finally, we design proof nets providing canonical representatives of derivations up to local rule permutations.