2024/11/13 by Acclavio, Matteo, Manara, Giulia
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2411.08847
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.