Parameterized Concurrent Multi-Party Session Types

TL;DR

This paper introduces System-A, a new session type system that effectively verifies complex, parameterized, asynchronous multi-party communication protocols, overcoming limitations of previous systems.

Contribution

System-A is a novel typing language that explicitly supports asynchrony, parallelism, and parameterization, enabling the static verification of a broader class of protocols.

Findings

System-A can verify protocols like sliding window that were previously inexpressible.

It supports multiple forms of parameterization and asynchronous communication.

Demonstrates effectiveness on a large class of asynchronous protocols.

Abstract

Session types have been proposed as a means of statically verifying implementations of communication protocols. Although prior work has been successful in verifying some classes of protocols, it does not cope well with parameterized, multi-actor scenarios with inherent asynchrony. For example, the sliding window protocol is inexpressible in previously proposed session type systems. This paper describes System-A, a new typing language which overcomes many of the expressiveness limitations of prior work. System-A explicitly supports asynchrony and parallelism, as well as multiple forms of parameterization. We define System-A and show how it can be used for the static verification of a large class of asynchronous communication protocols.