of multiplicative linear logic as typing system for concurrent functional programming. In
particular, we study a linear multiple-conclusion natural deduction system and show it is
isomorphic to a simple and natural extension of λ-calculus with parallelism and
communication primitives, called λpar. We shall prove that λpar satisfies all the desirable
properties for a typed programming language: subject reduction, progress, strong …