A carregar...
Publicação
Proof Nets as Processes
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 681.28 KB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
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.
Descrição
This 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.
Palavras-chave
Programming languages Proof nets Types Propositions as types Deterministic parallelism Pi calculus Process algebra Linear Logic