Multiparty Session Types with a Bang!

TL;DR

This paper extends Multiparty Session Types with type-level replication, enabling the expression of complex protocols like mutual exclusion and races, and explores its impact on typechecking and protocol expressiveness.

Contribution

It introduces MPST! with replication and first-class roles, showing its increased expressiveness and analyzing its effects on typechecking decidability.

Findings

Replication is not equivalent to recursion in MPST.

Using both replication and recursion allows expressing complex protocols.

Replication impacts the decidability of typechecking.

Abstract

Replication is an alternative construct to recursion for describing infinite behaviours in the pi-calculus. In this paper we explore the implications of including type-level replication in Multiparty Session Types (MPST), a behavioural type theory for message-passing programs. We introduce MPST!, a session-typed multiparty process calculus with replication and first-class roles. We show that replication is not an equivalent alternative to recursion in MPST, and that using both replication and recursion in one type system in fact allows us to express both context-free protocols and protocols that support mutual exclusion and races. We demonstrate the expressiveness of MPST! on examples including binary tree serialisation, dining philosophers, and a model of an auction, and explore the implications of replication on the decidability of typechecking.