On the \(\pi\)-calculus and linear logic (Q1342247)

The authors extend the Curry-Howard ``formulae-as-types/proofs-as- objects'' isomorphism to what Abramsky calls the ``proofs-as-processes'' paradigm, translating linear logic into the \(\pi\)-calculus. The \(\pi\)- calculus is a formalism, with the flavor of the \(\lambda\)-calculus, for capturing concurrency. The translation is done first for sequential linear logic proofs, then proof structures. In both cases first the multiplicatives are handled, then the additives, and lastly the exponentials, because the translations become ever less nice through these cases.