一句话：提出异步会话子类型的一种可靠但不完备的检查算法，并实现工具评估其适用性与开销。
会话类型用于描述分布式系统中通信端点的交互协议，其子类型关系能让更多行为相似但不完全一致的程序通过类型检查。然而，异步环境下的会话子类型已被证明是不可判定的。已有工作通过限制会话类型语法或采用有界异步通信来回避该问题，但实践限制过强。本文提出一种异步会话子类型的检查算法：该算法可靠但不完备，某些情况下会终止而不给出确定判定。它基于异步子类型余归纳定义的树表示，通过检测无限成功子树的有限见证来工作，并实现了相应工具。作者在以往方法无法处理的多个例子上进行测试，并对算法的时间和空间开销做了经验评估。
Session types, types for structuring communication between endpoints in distributed systems, are recently being integrated into mainstream programming languages. In practice, a very important notion for dealing with such types is that of subtyping, since it allows for typing larger classes of system, where a program has not precisely the expected behaviour but a similar one. Unfortunately, recent work has shown that subtyping for session types in an asynchronous setting is undecidable. To cope with this negative result, the only approaches we are aware of either restrict the syntax of session types or limit communication (by considering forms of bounded asynchrony). Both approaches are too restrictive in practice, hence we proceed differently by presenting an algorithm for checking subtyping which is sound, but not complete (in some cases it terminates without returning a decisive verdict). The algorithm is based on a tree representation of the coinductive definition of asynchronous subtyping; this tree could be infinite, and the algorithm checks for the presence of finite witnesses of infinite successful subtrees. Furthermore, we provide a tool that implements our algorithm. We use this tool to test our algorithm on many examples that cannot be managed with the previous approaches, and to provide an empirical evaluation of the time and space cost of the algorithm.Comment: This is an extended version of the CONCUR'19 version
@article{paperbot1331,
title = {A Sound Algorithm for Asynchronous Session Subtyping and its Implementation},
author = {Mario Bravetti and Marco Carbone and Julien Lange and Nobuko Yoshida and Gianluigi Zavattaro},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 1},
year = {2021},
doi = {10.23638/lmcs-17(1:20)2021}
}