Partial Typing for Asynchronous Multiparty Sessions
Franco Barbanera, Mariangiola Dezani-Ciancaglini, Ugo de'Liguoro
TL;DR
The paper tackles scalable verification of partial properties in asynchronous multiparty session types by introducing a partial typing framework that assigns asynchronous global types to subsystems described by a subset $\mathcal{P}$ of participants. It formalizes $\mathcal{P}$-lock-freedom and $\mathcal{P}$-orphan-message-freedom, and develops asynchronous global types together with a boundedness concept (via Paths and depth) and a weight-based notion to ensure $\mathcal{P}$-soundness. A history-based, implicitly coinductive type system is then presented to derive typings that respect queue invariants and prove key properties such as Subject Reduction, Session Fidelity, and the targeted partial properties. The approach enables verification of subsystem-level behavior in distributed settings without enforcing full-system guarantees, offering a scalable path for reasoning about real-world asynchronous interactions. The work extends MPST theory by focusing on partial properties and asynchronous semantics, with potential applications to complex subsystems where full verification is intractable.
Abstract
Formal verification methods for concurrent systems cannot always be scaled-down or tailored in order to be applied on specific subsystems. We address such an issue in a MultiParty Session Types setting by devising a partial type assignment system for multiparty sessions (i.e. sets of concurrent participants) with asynchronous communications. Sessions are possibly typed by "asynchronous global types" describing the overall behaviour of specific subsets of participants only (from which the word "partial"). Typability is proven to ensure that sessions enjoy the partial versions of the well-known properties of lock- and orphan-message-freedom.