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.

翻译：多方会话类型（MPST）为验证并发系统的安全性与活性提供了严格的理论基础。然而，现有方法往往迫使研究者面临两难选择：经典的基于投影的技术虽具备组合性，但表达能力有限；而近期技术虽通过依赖非组合性的全系统模型检查实现了更高的表达能力，却存在可扩展性差的问题。本文提出了一种称为综合方法的新型MPST方案，旨在同时实现表达能力和组合性。我们的核心创新在于设计了一个类型系统，可直接针对全局协议规范验证每个进程——该规范通常表示为带标签的转移系统（LTS），而全局类型可作为其特例。该方法独特地避免了中间局部类型与投影的需求。我们证明，尽管概念上更为简洁，我们的方法能够支持一系列具有挑战性的协议基准测试，这些协议在既往MPST文献中超出了组合性技术的处理范围。我们进一步推广该类型系统，表明其可验证进程是否符合任何构成“行为良好”LTS的规范，从而支持标准全局类型语法无法表达的协议。整个框架（包括所有定理及大量示例）已在Agda中完成形式化与机械化实现，并开发了作为VS Code扩展的原型实现。