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类型系统，并讨论了各自用于类型安全性证明的方法。