Proof Nets for PiL (Full Version)

TL;DR

This paper introduces proof nets for PiL, an extension of linear logic, enabling a canonical and efficient representation of process encodings in the pi-calculus.

Contribution

It presents a novel proof net framework for PiL with correctness, sequentialization, and translation algorithms, advancing the understanding of process encodings.

Findings

Proof nets provide a canonical representation of sequent calculus derivations.

The paper establishes correctness criteria and translation algorithms for PiL proof nets.

PiL proof nets facilitate shallow encoding of pi-calculus processes as formulas.

Abstract

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 {\pi}-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.