Propositions as sessions

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

Continuing a line of work by Abramsky (1994), Bellin and Scott (1994), and 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), Honda et al. (1998), and Gay & Vasconcelos (2010), among others, this paper presents GV, a linear functional language with session types, and 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 yields a language free from races and deadlock, where race and deadlock freedom follows from the correspondence to linear logic.
Original languageEnglish
Pages (from-to)384-418
Number of pages35
JournalJournal of Functional Programming
Issue numberSpecial Issue 2-3
Early online date31 Jan 2014
Publication statusPublished - May 2014


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

Cite this