Synchronous Multiparty Session Types
Synchronous Multiparty Session Types
复制标题
DOI：
10.1016/j.entcs.2009.06.002
复制
发表时间：
2009-07
影响因子：
--
通讯作者：
Andi Bejleri;N. Yoshida
中科院分区：
文献类型：
--
作者：
Andi Bejleri;N. Yoshida
同步通信对于建模多方会话很有用，其中控制定时事件和消息的强顺序对于问题规范是必不可少的。本文继续了本田等人[本田，K.，N. Yoshida和M. Carbone，多方异步会话类型，在：G。C. Necula和P. Wadler，编辑，POPL（2008），第100页。273-284]用于同步通信。它提供了一种更宽松的演算语法，多播，通过多极标签进行高阶通信，以及全局类型中委托的明确定义。linearity属性定义了什么时候一个通道可以在两个不同的通信中使用而不创建争用条件，并且类型系统检查会话的所有进程是否实现了全局类型中指定的通信行为。演算的类型系统被证明是健全的相对于操作语义和一致的相对于全局类型。
Synchronous communication is useful to model multiparty sessions where control for timing events and strong sequentially order of messages are essential to the problem specification. This paper continues the work on multiparty session types initiated by Honda et al. [Honda, K., N. Yoshida and M. Carbone, Multiparty asynchronous session types, in: G. C. Necula and P. Wadler, editors, POPL (2008), pp. 273–284] for synchronous communications. It provides a more relaxed syntax of the calculus, multicasting, higher-order communication via multipolarity labels and a clear definition of delegation in global types. The linearity property defines when a channel can be used in two different communications without creating a race condition and the type system checks if all the processes of a session implement the communication behavior specified in the global type. The type system of the calculus is proved to be sound with respect to the operational semantics and coherent with respect to the global types.