Linearly Typed Dyadic Group Sessions for Building Multiparty Sessions

• Main Authors: Xi, Hongwei, Wu, Hanwen
• Format: Report
• Language: unknown
• Published: arXiv 2016
• Subjects: Programming Languages cs.PL; FOS Computer and information sciences; Lambda; DML
• Online Access: https://dx.doi.org/10.48550/arxiv.1604.03020; https://arxiv.org/abs/1604.03020

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. : This paper can be seen as the pre-sequel to classical linear multirole logic (CLML). arXiv admin note: substantial text overlap with arXiv:1603.03727