Mostrous, Dimitris2012-10-312014-11-142012-10-312014-11-142012-10-31http://hdl.handle.net/10451/14180http://repositorio.ul.pt/handle/10455/6890This work describes a process algebraic interpretation of Proof-nets, which are the canonical objects of Linear Logic proofs. It therefore offers a logically founded basis for deterministic, implicit parallelism.We present delta-calculus, a novel interpretation of Linear Logic, in the form of a typed process algebra that enjoys a Curry-Howard correspondence with Proof Nets. Reduction inherits the qualities of the logical objects: termination, deadlock-freedom, determinism, and very importantly, a high degree of parallelism. We obtain the necessary soundness results and provide a propositions-as-types theorem. The basic system is extended in two directions. First, we adapt it to interpret Affine Logic. Second, we propose extensions for general recursion, and introduce a novel form of recursive linear types. As an application we show a highly parallel type-preserving translation from a linear System F and extend it to the recursive variation. Our interpretation can be seen as a more canonical proof-theoretic alternative to several recent works on pi-calculus interpretations of linear sequent proofs (propositions-as-sessions) which exhibit reduced parallelism.engProgramming languagesProof netsTypesPropositions as typesDeterministic parallelismPi calculusProcess algebraLinear Logicreport