用于构建多方会话的线性类型的二元组会话
Linearly Typed Dyadic Group Sessions for Building Multiparty Sessions
摘要：
传统上，（二元或多方）会话中的每一方都只实现会话类型中指定的一个角色。我们将这种会话称为单独会话（i-session）。作为i-会话的概括，组会话（g-会话）是其中每一方可以基于一个通道实现一组角色的会话。特别地，参与二元g会话的双方中的每一方实现一组角色或其补充。在本文中，我们提出了一个形式化的g-会话在多线程并行演算（MTLC）配备了线性类型系统，建立MTLC的类型保存和全球的进展。由于这个制定MTLC可以很容易地嵌入到ATS，一个功能齐全的编程语言的核心，支持依赖类型（的DML风格）和线性类型，我们得到了一个直接实现的线性类型的G-会话在ATS。本文的主要贡献在于确定的g-会议作为一个基本的构建块多方会议和理论发展，支持这种识别。
英文摘要：
Traditionally, each party in a (dyadic or multiparty) session implements exactly one role specified in the type of the session. We refer to this kind of session as an individual session (i-session). As a generalization of i-session, a group session (g-session) is one in which each party may implement a group of roles based on one channel. In particular, each of the two parties involved in a dyadic g-session implements either a group of roles or its complement. In this paper, we present a formalization of g-sessions in a multi-threaded lambda-calculus (MTLC) equipped with a linear type system, establishing for the MTLC both type preservation and global progress. As this formulated MTLC can be readily embedded into ATS, a full-fledged language with a functional programming core that supports both dependent types (of DML-style) and linear types, we obtain a direct implementation of linearly typed g-sessions in ATS. The primary contribution of the paper lies in both of the identification of g-sessions as a fundamental building block for multiparty sessions and the theoretical development in support of this identification.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
