  Along the lines of the Abramsky ``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
multiple-conclusion natural deduction system and show it is isomorphic to a
simple and natural extension of $\lambda$-calculus with parallelism and
communication primitives, called $\lambda_{\unicode{8523}}$. We shall prove
that $\lambda_{\unicode{8523}}$ satisfies all the desirable properties for a
typed programming language: subject reduction, progress, strong normalization
and confluence.
