精确的混合选择多方会话类型
Mixed Choice Multiparty Session Types, Precisely
AI总结：
本文针对含会话委托等特性的混合选择多方会话类型，证明其子类型关系的精确性，开发通用类型系统并实现相关检查算法，经案例研究验证其有效性。
AI中文摘要：
精确（可靠且完备）的子类型关系≤规定，当且仅当类型为T'的程序总能安全替换类型为T的程序，且不会损害更大程序的安全性时，T'是T的子类型。本文针对具备会话委托、创建和交错特性的混合选择多方会话类型，构建并证明其子类型关系的精确性。我们通过为完整的混合选择多方会话π演算开发首个通用类型系统来证明可靠性；为证明完备性，引入三方锁——这是处理交错会话的最小且通用的活性错误形式，并基于调度器进程的构建建立新的证明技术，该技术可对子类型关系的所有失败情况进行穷尽检测。随后，我们将精确性结果扩展至一类混合选择多方会话类型。用于检查（1）子类型关系，以及（2）类型上下文的安全性、无死锁性和活性的算法已全部实现并优化，其运行时间相对于状态空间和类型上下文的规模为二次复杂度，且已通过文献中的（混合选择）案例研究进行评估。
英文摘要：
A precise (sound and complete) subtyping relation $\leq$ specifies that $T'$ is a subtype of $T$ if and only if a program of type $T'$ can always safely replace a program of type $T$ without compromising the safety of a larger program. This paper formulates and proves preciseness of subtyping for mixed choice multiparty session types with session delegation, creation, and interleaving. We prove soundness by developing the first general type system for a full mixed choice multiparty session $π$-calculus. To prove completeness, we introduce the three-party lock, which is a minimal and general form of liveness error for handling interleaved sessions, and we establish a new proof technique based on a construction of scheduler processes which enable exhaustive detection for all failures of the subtyping relation. We then extend the preciseness results to a family of mixed choice multiparty session types. Algorithms for checking (1) subtyping and (2) safety, deadlock-freedom, and liveness of typing contexts are fully implemented and optimised to run in quadratic time with respect to the size of the state space and typing context, and have been evaluated with (mixed choice) case studies from the literature.
