Utilize este identificador para referenciar este registo: http://hdl.handle.net/10451/14180
Título: Proof Nets as Processes
Autor: Mostrous, Dimitris
Palavras-chave: Programming languages
Proof nets
Types
Propositions as types
Deterministic parallelism
Pi calculus
Process algebra
Linear Logic
Data: 31-Out-2012
Relatório da Série N.º: 2012;07
Resumo: 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.
URI: http://hdl.handle.net/10451/14180
http://repositorio.ul.pt/handle/10455/6890
Aparece nas colecções:FC-DI - Technical Reports

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
Proof Nets as Processes TR.pdf681,28 kBAdobe PDFVer/Abrir


FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpace
Formato BibTex MendeleyEndnote Degois 

Todos os registos no repositório estão protegidos por leis de copyright, com todos os direitos reservados.