Par means parallel: Multiplicative linear logic proofs as concurrent functional programs

Abstract

Along the lines of Abramsky's "Proofs-as-Processes" program, we present an interpretation of multiplicative linear logic as typing system for concurrent functional programming. In particular, we study a linear multipleconclusion natural deduction system and show it is isomorphic to a simple and natural extension of γ-calculus with parallelism and communication primitives, called γ. We shall prove that γ satisfies all the desirable properties for a typed programming language: subject reduction, progress, strong normalization and confluence.