Proof Nets in Process Algebraic Form

Abstract. We present δ-calculus, a computational interpretation of Lin-ear Logic, in the form of a typed process algebra whose structures corre-spond to Proof Nets, and where typing derivations correspond to linear sequent proofs. Term reduction shares the properties of cut elimination in the logic, and immediately we can obtain a number of inherited quali-ties, among which are termination, deadlock-freedom, and determinism. We obtain the expected soundness results and provide a propositions-as-types correspondence theorem. We then propose extensions for general recursion and the removal of the additive fragment while allowing to express similar behaviour, contributing to the theory of proof nets.