Propositions as sessions
Propositions as sessions
复制标题
提案作为会议
DOI：
--
复制
发表时间：
2012
影响因子：
1.1
通讯作者：
P. Wadler
中科院分区：
文献类型：
--
作者：
S. Fowler;S. Lindley;P. Wadler
继续Abramsky（1994）、贝林和Scott（1994）以及Caires和Pfenning（2010）等人的工作，本文提出了CP，一种经典线性逻辑的命题对应于会话类型的演算。继续本田（1993），本田，久保，和Vasconcelos（1998），和Gay和Vasconcelos（2010）的工作，在其他人中，本文介绍了GV，一个具有会话类型的线性函数语言，并提出了从GV到CP的翻译。翻译第一次正式的会话类型和线性逻辑的标准表示之间的连接，并显示了如何修改标准表示产生一个无死锁的语言，其中死锁自由遵循对应线性逻辑。
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.