MAG$\pi$!: The Role of Replication in Typing Failure-Prone Communication

TL;DR

MAG$\pi$! extends the multiparty session types framework by integrating replication, enabling more flexible modeling of failure-prone, infinitely available communication protocols with proven safety properties.

Contribution

It introduces replication into multiparty session types, simplifying the specification of distributed client-server interactions and proving key safety properties.

Findings

Type system guarantees handling of message loss via timeouts

Replication simplifies specification of distributed interactions

Proven properties include subject reduction and session fidelity

Abstract

MAG$\pi$ is a Multiparty, Asynchronous and Generalised $\pi$-calculus that introduces timeouts into session types as a means of reasoning about failure-prone communication. Its type system guarantees that all possible message-loss is handled by timeout branches. In this work, we argue that the previous is unnecessarily strict. We present MAG$\pi$!, an extension serving as the first introduction of replication into Multiparty Session Types (MPST). Replication is a standard $\pi$-calculus construct used to model infinitely available servers. We lift this construct to type-level, and show that it simplifies specification of distributed client-server interactions. We prove properties relevant to generalised MPST: subject reduction, session fidelity and process property verification.