自上而下 = 自下而上：多方全局协议对活性的合理且完备的刻画
Top-down = Bottom-up: Sound and Complete Characterisations of Liveness by Multiparty Global Protocols
浏览论文内容
中文总结 AI 辅助
研究多方会话类型中自上而下与自下而上策略的可类型化性，通过主全局类型推断算法证明二者相同，实现相关算法并构建工具链，经评估发现自上而下方法比自下而上方法更高效。
中文摘要 AI 辅助
多方会话类型（MPST）是并发和分布式系统的一种类型规范，旨在确保类型安全、无死锁以及类型化通信进程的活性。已提出两种主要的MPST方法，自上而下和自下而上，并已集成到多种编程语言和工具中。自上而下策略从指定协议的整体编排（称为全局类型）开始，通过端点投影（EPP）生成一组满足安全性和活性的局部类型。对每个参与者进行类型检查后，进程集的活性自动得到保证。自下而上策略直接检查从进程推断出的局部类型是否满足活性。通常认为自上而下系统的可类型化性比自下而上系统严格更低。本文否定了这一观点。我们证明，使用精确的子类型包含规则，自上而下策略提供与自下而上系统完全相同的可类型化性。更确切地说，当且仅当多方会话\(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 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 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.
