Propositions as sessions*. Issue 2 (31st January 2014)

• Record Type: Journal Article
• Authors: WADLER, PHILIP
• Is Part Of: Journal of functional programming. Volume 24:Issue 2/3(2014)
• Page Start: 384
• Page End: 418
• Publication Date: 2014-01-31
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S095679681400001X
• Languages: English
• ISSNs: 0956-7968

Abstract

Abstract: 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.