一句话：首次形式化异步多方会话的精确子类型，并证明其可靠且完备，实现安全进程替换与异步消息优化。
会话子类型是通信进程精化的基础：若 T 是 T′ 的子类型，则可在期望 T′ 的上下文中安全替换为 T 的实现，避免死锁与通信错误。此前精确子类型仅覆盖二元会话或同步多方会话。本文首次形式化异步多方会话的精确子类型，其中消息经 FIFO 队列传输。异步环境下参与者可重排输入输出而不引发错误，精确定义必须捕获所有合法排列，因而极具挑战。作者提出会话分解技术，将含内部/外部选择的会话类型分解为无选择的单一输入/输出会话树，并以树间精化关系的组合定义子类型。结果证明该子类型可靠且完备：任何扩展都不安全；并在操作语义与指称语义上均精确。
Session subtyping is a cornerstone of refinement of communicating processes: a process implementing a session type (i.e., a communication protocol) T can be safely used whenever a process implementing one of its supertypes T ′ is expected, in any context, without introducing deadlocks nor other communication errors. As a consequence, whenever T T ′ holds, it is safe to replace an implementation of T ′ with an implementation of the subtype T , which may allow for more optimised communication patterns. We present the first formalisation of the precise subtyping relation for asynchronous multiparty sessions. We show that our subtyping relation is sound (i.e., guarantees safe process replacement, as outlined above) and also complete : any extension of the relation is unsound. To achieve our results, we develop a novel session decomposition technique, from full session types (including internal/external choices) into single input/output session trees (without choices). Previous work studies precise subtyping for binary sessions (with just two participants), or multiparty sessions (with any number of participants) and synchronous interaction. Here, we cover multiparty sessions with asynchronous interaction, where messages are transmitted via FIFO queues (as in the TCP/IP protocol), and prove that our subtyping is both operationally and denotationally precise. In the asynchronous multiparty setting, finding the precise subtyping relation is a highly complex task: this is because, under some conditions, participants can permute the order of their inputs and outputs, by sending some messages earlier or receiving some later, without causing errors; the precise subtyping relation must capture all such valid permutations — and consequently, its formalisation, reasoning and proofs become challenging. Our session decomposition technique overcomes this complexity, expressing the subtyping relation as a composition of refinement relations between single input/output trees, and providing a simple reasoning principle for asynchronous message optimisations.
@article{paperbot1186,
title = {Precise subtyping for asynchronous multiparty sessions},
author = {Silvia Ghilezan and Jovanka Pantović and Ivan Prokić and Alceste Scalas and Nobuko Yoshida},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434297}
}