Ensuring correctness of communication in distributed systems remains challenging. To address this, Multiparty session types (MPST), initially introduced by Honda et al. [52, 53], offer a type discipline in which a programmer or architect specifies an overall view of communication as a global protocol (global type), and each distributed program is locally type-checked against its end-point projection. In practice, the MPST framework has been integrated into over 25 programming languages or tools. Ten years after the emergence of MPST, Scalas and Yoshida [84] discovered that existing proofs of type safety using end-point projection with mergeability are flawed, where the mergeability operator enlarges the typability of MPST end-point programs, admits easy implementation, and is more efficient than alternative approaches, including model checking. Nevertheless, following the result in [84], the soundness of end-point projection (with mergeability) has been interpreted in the literature as problematic. We clarify this concern by proposing a new general proof technique for type soundness (subject reduction) of multiparty session $π$-calculus, which relies on an association relation between the behavioural semantics of a global type and its end-point projection. With this approach, behavioural properties, namely session fidelity, deadlock freedom, and liveness, are also guaranteed based on global types. Additionally, we provide detailed comparisons with existing MPST typing systems and discuss their respective proof methods for type soundness.

翻译：分布式系统中通信正确性的保障仍然具有挑战性。为此，由Honda等人[52, 53]最初提出的多会话类型（MPST）提供了一种类型规范，程序员或架构师可通过全局协议（全局类型）指定通信的全局视图，每个分布式程序则通过其端点投影进行局部类型检查。实践中，MPST框架已被集成到超过25种编程语言或工具中。在MPST出现十年后，Scalas与Yoshida[84]发现，现有使用可合并性端点投影的类型安全性证明存在缺陷——可合并性算子扩大了MPST端点程序的可类型化范围，易于实现，且比包括模型检测在内的替代方法更高效。然而，[84]的研究结果导致文献中将（带可合并性的）端点投影的合理性解读为存在问题。本文通过提出一种多会话π演算类型安全性（主体归约）的通用新证明技术来澄清此问题，该技术基于全局类型行为语义与其端点投影之间的关联关系。采用该方法后，基于全局类型还可保证会话保真性、无死锁性及活性等行为属性。此外，我们与现有MPST类型系统进行了详细比较，并讨论了各自类型安全性的证明方法。