A Synthetic Reconstruction of Multiparty Session Types (with Appendix)
David Castro-Perez, Francisco Ferreira, Sung-Shik Jongmans
TL;DR
Safety and liveness verification for multiparty protocols typically forces a trade-off between compositional projection-based MPST and more expressive whole-system approaches. This paper introduces a synthetic MPST approach that verifies each process directly against a global protocol specification, represented as a labelled transition system (LTS), eliminating the need for intermediate local types or projections. The framework generalizes to any well-behaved LTS, enabling protocols not expressible with standard global type syntax, while preserving compositional reasoning. The authors formalize theorems and examples in Agda and provide a practical prototype as a VS Code extension. Empirically, the synthetic approach handles challenging protocols beyond prior MPST techniques, laying groundwork for broader applicability of MPST through semantic specifications.
Abstract
Multiparty session types (MPST) provide a rigorous foundation for verifying the safety and liveness of concurrent systems. However, existing approaches often force a difficult trade-off: classical, projection-based techniques are compositional but limited in expressiveness, while more recent techniques achieve higher expressiveness by relying on non-compositional, whole-system model checking, which scales poorly. This paper introduces a new approach to MPST that delivers both expressiveness and compositionality, called the synthetic approach. Our key innovation is a type system that verifies each process directly against a global protocol specification, represented as a labelled transition system (LTS) in general, with global types as a special case. This approach uniquely avoids the need for intermediate local types and projection. We demonstrate that our approach, while conceptually simpler, supports a benchmark of challenging protocols that were previously beyond the reach of compositional techniques in the MPST literature. We generalise our type system, showing that it can validate processes against any specification that constitutes a "well-behaved" LTS, supporting protocols not expressible with the standard global type syntax. The entire framework, including all theorems and many examples, has been formalised and mechanised in Agda, and we have developed a prototype implementation as an extension to VS Code.