In this paper, we establish the foundations of a novel logical framework for the {\pi}-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.

翻译：本文基于“演绎即计算”范式，为π演算建立了一种新型逻辑框架的基础。遵循逻辑编程的标准证明论解释，我们将进程表示为公式，并将证明解释为计算。为此，我们为一阶乘性加性线性逻辑的扩展定义了一种无切割的矢列演算。该扩展包含一个非交换且非结合的连接词以忠实建模前缀算子，并包含名义量词以表示名称限制。最后，我们设计了证明网，为局部规则置换下的推导提供了典范表示。