この論文をさがす
説明
<jats:title>Abstract</jats:title><jats: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<jats:italic>et al</jats:italic>. (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.</jats:p>
収録刊行物
-
- Journal of Functional Programming
-
Journal of Functional Programming 24 (2-3), 384-418, 2014-01-31
Cambridge University Press (CUP)
