Propositions as Sessions

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

Continuing a line of work by Abramsky (1994), by Bellin and Scott (1994), and by Caires and Pfenning (2010), among others, this paper presents CP, a calculus in which propositions of classical linear logic correspond to session types. Continuing a line of work by Honda (1993), by Honda, Kubo, and Vasconcelos (1998), and by Gay and Vasconcelos (2010), among others, this paper presents GV, a linear functional language with session types, and presents a translation from GV into CP. The translation formalises for the first time a connection between a standard presentation of session types and linear logic, and shows how a modification to the standard presentation yield a language free from deadlock, where deadlock freedom follows from the correspondence to linear logic.
Original languageEnglish
Title of host publicationICFP '12 Proceedings of the 17th ACM SIGPLAN international conference on Functional programming
Number of pages14
ISBN (Print)978-1-4503-1054-3
Publication statusPublished - Sept 2012


Dive into the research topics of 'Propositions as Sessions'. Together they form a unique fingerprint.

Cite this