一句话：提出更简单且更通用的多方会话类型理论，去除全局类型与二元对偶，修复类型安全证明缺陷，并支持可判定类型检查与活性保证。
经典多方会话类型（MPST）用类型保证消息传递进程正确实现多方会话协议，但其理论基础存在严重局限：主题归约性质受限，隐含限制容易被忽略，已有工作甚至因此出现类型安全证明缺陷。本文重新审视 MPST，提出一个更简单却更通用的理论：它不要求全局多方会话类型，也不依赖二元会话类型对偶，而是基于一般行为类型级性质，从而能证明更多协议和进程的类型安全。作者进一步分析这些类型级性质，说明它们如何保证类型检查可判定，并静态确保运行时无死锁与活性。最后展示新理论可整合类型与模型检查，将类型级性质表达为模态 μ 演算，并用成熟工具验证。
Multiparty Session Types (MPST) are a typing discipline ensuring that a message-passing process implements a multiparty session protocol , without errors. In this paper, we propose a new, generalised MPST theory. Our contribution is fourfold. (1) We demonstrate that a revision of the theoretical foundations of MPST is necessary : classic MPST have a limited subject reduction property, with inherent restrictions that are easily overlooked, and in previous work have led to flawed type safety proofs; our new theory removes such restrictions and fixes such flaws. (2) We contribute a new MPST theory that is less complicated, and yet more general, than the classic one: it does not require global multiparty session types nor binary session type duality — instead, it is grounded on general behavioural type-level properties, and proves type safety of many more protocols and processes. (3) We produce a detailed analysis of type-level properties, showing how, in our new theory, they allow to ensure decidability of type checking, and statically guarantee that processes enjoy, , deadlock-freedom and liveness at run-time. (4) We show how our new theory can integrate type and model checking: type-level properties can be expressed in modal µ-calculus, and verified with well-established tools.