Parameterised Multiparty Session Types

TL;DR

This paper introduces a dependent type theory for multiparty session types that allows static guarantees of type safety and deadlock freedom in protocols with parameters known only at runtime, using recursion for complex patterns.

Contribution

It develops a dependent type system with recursion for multiparty sessions, enabling static verification of parameterized, dynamic communication protocols.

Findings

Type checking terminates for the full system.

Supports a wide range of communication patterns.

Validated with examples from parallel algorithms and Web services.

Abstract

For many application-level distributed protocols and parallel algorithms, the set of participants, the number of messages or the interaction structure are only known at run-time. This paper proposes a dependent type theory for multiparty sessions which can statically guarantee type-safe, deadlock-free multiparty interactions among processes whose specifications are parameterised by indices. We use the primitive recursion operator from G\"odel's System T to express a wide range of communication patterns while keeping type checking decidable. To type individual distributed processes, a parameterised global type is projected onto a generic generator which represents a class of all possible end-point types. We prove the termination of the type-checking algorithm in the full system with both multiparty session types and recursive types. We illustrate our type theory through non-trivial programming and verification examples taken from parallel algorithms and Web services usecases.