Propositions as sessions

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. Categories and Subject Descriptors F.4.1 [Mathematical Logic]: Lambda calculus and related systems; F.4.1 [Mathematical Logic]: Proof theory; D.3.3 [Language Constructs and Features]: Concurrent programming structures Ke...

• Type: Journal
• Year: 2012
• Where: ICFP
• Authors: Philip Wadler
• Keywords: Classical Linear Logic, ICFP 2012, Lambda Calculus, Linear Functional Language, Programming Languages