13.3.12

 

Propositions as Sessions

I've just released a draft paper. Comments welcome!
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

Comments:
Small typo. It's Peirce not Pierce.

I'm sure Benjamin C. would like the credit, but it belongs to Charles S. ;-)
 
Thanks Marc. Typo now corrected, and acknowledgement to you added.
 
There seems to be an extraneous "s" attached to the second occurrence of "forward" in the sentence "Whereas we forward any number of times and in either direction, they forwards only once and from X to X" on page 3.
 
Michael, Thanks. Typo fixed and your name added to acknowledgements.
 
Post a Comment

<< Home

This page is powered by Blogger. Isn't yours?