Multiparty asynchronous session types
Multiparty asynchronous session types
复制标题
DOI：
10.1145/1328438.1328472
复制
发表时间：
2008-01
期刊：
影响因子：
--
通讯作者：
Kohei Honda;N. Yoshida;Marco Carbone
中科院分区：
文献类型：
--
作者：
Kohei Honda;N. Yoshida;Marco Carbone
沟通正成为软件开发中的中心要素之一。作为以结构化通信为中心的编程的潜在打字基础，在过去的十年中，已经研究了会话类型，用于多种过程计算语言和编程语言，重点关注二进制（两部分）会话。这项工作将上述二进制会话类型的理论扩展到多方，异步会话，这些会话通常在以交流为中心的应用中出现。该理论作为移动过程的打字积分呈现，引入了一种新的类型概念，其中涉及多个同龄人的相互作用直接被抽象为全球场景。全局类型保留了二进制会话类型的友好类型语法，同时捕获多方异步相互作用的复杂因果链。全球类型在交流同龄人之间扮演共同协议的角色，并用作通过对单个同龄人投射的有效类型进行检查的基础。会话类型纪律的基本特性，例如通信安全，进度和会话保真度，用于将军派对异步相互作用。
Communication is becoming one of the central elements in software development. As a potential typed foundation for structured communication-centred programming, session types have been studied over the last decade for a wide range of process calculi and programming languages, focussing on binary (two-party) sessions. This work extends the foregoing theories of binary session types to multiparty, asynchronous sessions, which often arise in practical communication-centred applications. Presented as a typed calculus for mobile processes, the theory introduces a new notion of types in which interactions involving multiple peers are directly abstracted as a global scenario. Global types retain a friendly type syntax of binary session types while capturing complex causal chains of multiparty asynchronous interactions. A global type plays the role of a shared agreement among communication peers, and is used as a basis of efficient type checking through its projection onto individual peers. The fundamental properties of the session type discipline such as communication safety, progress and session fidelity are established for generaln-party asynchronous interactions.