Multiparty Session Types, Beyond Duality (Abstract)

TL;DR

This paper introduces a novel Multiparty Session Types system that overcomes the limitations of existing duality constraints, enabling more flexible and accurate typing of message-passing protocols involving multiple participants.

Contribution

It proposes a new MPST typing framework that removes duality restrictions, allowing for broader and more intuitive protocol typing in multiparty interactions.

Findings

Existing MPST restricts protocols due to duality constraints.

The new system relaxes these constraints, broadening applicability.

Preliminary analysis shows improved protocol expressiveness.

Abstract

Multiparty Session Types (MPST) are a well-established typing discipline for message-passing processes interacting on sessions involving two or more participants. Session typing can ensure desirable properties: absence of communication errors and deadlocks, and protocol conformance. However, existing MPST works provide a subject reduction result that is arguably (and sometimes, surprisingly) restrictive: it only holds for typing contexts with strong duality constraints on the interactions between pairs of participants. Consequently, many "intuitively correct" examples cannot be typed and/or cannot be proved type-safe. We illustrate some of these examples, and discuss the reason for these limitations. Then, we outline a novel MPST typing system that removes these restrictions.