Propositions as sessions*. Issue 2 (May 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-05
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S095679681400001X
• Languages: English
• ISSNs: 0956-7968

Abstract

<abstract abstract-type="normal"> <title>Abstract</title> <p>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 <italic>et al</italic>. (1998), and Gay &amp; 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.</p> </abstract>