Utilize este identificador para referenciar este registo: http://hdl.handle.net/10362/15296
Título: A logical foundation for session-based concurrent computation
Autor: Toninho, Bernardo Parente Coutinho Fernandes
Orientador: Pfenning, Frank
Caires, Luís
Palavras-chave: Linear logic
Session types
Curry-Howard
Concurrency
Proofs-as-programs
Data de Defesa: Mai-2015
Resumo: Linear logic has long been heralded for its potential of providing a logical basis for concurrency. While over the years many research attempts were made in this regard, a Curry-Howard correspondence between linear logic and concurrent computation was only found recently, bridging the proof theory of linear logic and session-typed process calculus. Building upon this work, we have developed a theory of intuitionistic linear logic as a logical foundation for session-based concurrent computation, exploring several concurrency related phenomena such as value-dependent session types and polymorphic sessions within our logical framework in an arguably clean and elegant way, establishing with relative ease strong typing guarantees due to the logical basis, which ensure the fundamental properties of type preservation and global progress, entailing the absence of deadlocks in communication. We develop a general purpose concurrent programming language based on the logical interpretation, combining functional programming with a concurrent, session-based process layer through the form of a contextual monad, preserving our strong typing guarantees of type preservation and deadlock-freedom in the presence of general recursion and higher-order process communication. We introduce a notion of linear logical relations for session typed concurrent processes, developing an arguably uniform technique for reasoning about sophisticated properties of session-based concurrent computation such as termination or equivalence based on our logical approach, further supporting our goal of establishing intuitionistic linear logic as a logical foundation for sessionbased concurrency.
URI: http://hdl.handle.net/10362/15296
Designação: Dissertação
Aparece nas colecções:FCT: DI - Teses de Doutoramento

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
Toninho_2015.pdf1,04 MBAdobe PDFVer/Abrir


FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpace
Formato BibTex MendeleyEndnote 

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