We introduce proof nets for PiL, an extension of first-order multiplicative additive linear logic with new operators allowing a shallow encoding of processes in the π-calculus as formulas. We provide correctness criterion, sequentialization procedure, and a proof translation algorithm. We show that proof nets provide a canonical representation of sequent calculus derivations modulo rule permutations.

翻译：我们为PiL引入证明网，PiL是一阶乘法加法线性逻辑的扩展，新增了算子允许将π演算中的进程浅层编码为公式。我们提供了正确性准则、序列化过程及证明翻译算法。我们证明证明网提供了规则置换下相继式演算推导的规范表示。