一句话：证明自顶向下与自底向上多参与者会话类型系统在活性上具有完全相同的可类型化能力。
多参与者会话类型（MPST）是一类用于并发与分布式系统的类型规约，旨在保证类型安全、无死锁以及通信进程的活性。已有自顶向下与自底向上两种主要方法：前者从全局类型出发，经端点投影生成局部类型并据此类型检查进程；后者直接从进程推断局部类型并检查其活性。学界长期认为，由于依赖全局类型与投影算法，自顶向下系统的可类型化能力严格弱于自底向上系统。本文否定这一看法：在子类型规则采用精确子类型时，自顶向下与自底向上具有完全相同的可类型化能力，即一个多参与者会话 M 被自底向上系统类型检查并通过活性验证，当且仅当它可被自顶向下系统类型检查。证明关键在于提出主全局类型推断算法，能从任意一组活性局部类型构造出主全局类型。作者实现了该推断算法以及投影、进程类型检查与局部类型推断，构建了支持两种策略的工具链，并用文献中的代表性例子评估，确认自顶向下方法比自底向上方法更高效。
Multiparty session types (MPST) are a type discipline for concurrent and distributed systems, designed to ensure not only type safety and deadlock-freedom, but also liveness of typed communicating processes. Two main MPST methodologies, top-down and bottom-up, have been proposed and are integrated into a wide range of programming languages and tools. The top-down strategy starts by specifying the overall choreography of the protocol (called a global type), from which a set of local types that satisfy safety and liveness are generated by endpoint projection (EPP). Once each participant is type-checked against a generated local type, liveness of the set of typed processes is automatically ensured by construction . The bottom-up strategy directly checks whether local types inferred from processes satisfy liveness in order to enforce liveness of processes. Since the top-down strategy depends on global types and the EPP algorithms, it has often been considered that the top-down system offers strictly less typability than the bottom-up system. Our paper negates this belief. We prove that, using the precise subtyping for the subsumption rule, the top-down strategy offers exactly the same typability as the bottom-up system. More precisely, a multiparty session M is typable and verified to be live by the bottom-up typing system if and only if M is typable by the top-down typing system. The key to the proof is the development of a principal global type inference algorithm which builds a principal global type from an arbitrary set of live local types. We have implemented the global type inference algorithm together with projection, process type checking and local type inference algorithms, and built a toolchain for both the top-down and bottom-up strategies. We evaluated our toolchain with representative examples from the literature, confirming that the top-down approach is more efficient than the bottom-up approach.
@article{paperbot12081,
title = {Top-Down = Bottom-Up: Sound and Complete Characterisations of Liveness by Multiparty Global Protocols},
author = {Kai Pischke and Nobuko Yoshida},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839538}
}