Linearly Typed Dyadic Group Sessions for Building Multiparty Sessions

TL;DR

This paper introduces a formalization of group sessions (g-sessions) in a multi-threaded lambda-calculus with linear types, enabling direct implementation of multiparty sessions in ATS, a language supporting dependent and linear types.

Contribution

It formalizes g-sessions as a fundamental component for multiparty sessions and develops a type-safe framework within MTLC and ATS for their implementation.

Findings

Established type preservation and global progress in MTLC with linear types.

Embedded g-sessions into ATS for practical implementation.

Identified g-sessions as key for multiparty session building.

Abstract

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.