通过共享会话类型进行明显的分阶段通信
Manifestly Phased Communication via Shared Session Types
摘要：
会话类型表示并发进程之间的消息协议，允许进程间通信的类型安全表达式。虽然以前的工作证明了一个定义良好的概念，子类型的过程中有不同的看法的协议，这些配方仅限于线性会话类型的每个通信渠道有一个独特的提供者和客户端。在本文中，我们将子类型扩展到共享会话类型，其中通道现在可以具有多个客户端而不是单个客户端。我们证明，这种泛化可以静态捕获协议的要求，跨越多个阶段的客户端与共享服务提供商的交互，这是不可能在以前的建议。此外，这些阶段在客户端的类型中很明显。
英文摘要：
Session types denote message protocols between concurrent processes, allowing a type-safe expression of inter-process communication. Although previous work demonstrate a well-defined notion of subtyping where processes have different perceptions of the protocol, these formulations were limited to linear session types where each channel of communication has a unique provider and client. In this paper, we extend subtyping to shared session types where channels can now have multiple clients instead of a single client. We demonstrate that this generalization can statically capture protocol requirements that span multiple phases of interactions of a client with a shared service provider, something not possible in prior proposals. Moreover, the phases are manifest in the type of the client.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
