Bernardo Toninho (Carnegie Mellon University), Linear Logic: A logical foundation for concurrent computation



Linear logic has long been heralded as a potential model for concurrency: from Girard's original paper, to Abramsky's computational interpretation, reiterated by Bellin and Scott. More recently, an interpretation for intuitionistic linear logic has been given by Caires and Pfenning where propositions are viewed as session types - a well established typing discipline for concurrency - proofs as processes and proof reduction as inter-process communication. In this talk I will detail how this interpretation can form a basis to a logical foundation that captures several interesting features of concurrency and concurrent computation. Specifically, I will detail how one can capture concurrent evaluation strategies for functional computation through canonical logical translations; the relationship between isomorphisms in linear logic and (typed) process equivalence; how asynchronous communication can be interpreted logically and sketch how the interpretation can be extended to richer typed settings such as dependent type theories.