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.

翻译：分布式系统端点之间沟通结构的会话类型、 分布式系统端点之间的沟通类型,最近正在被纳入主流编程语言中。 实际上,处理这类类型的一个非常重要的概念是亚型,因为它允许打入较大的系统类别,而一个程序并不精确预期的行为,但相似的行为。 不幸的是,最近的工作表明,在一个不同步的环境中对会话类型进行分解是不可分化的。为了应对这一负面结果,我们所了解的唯一限制会话类型组合或限制通信的方法(考虑到受约束的无节制形式)在实践上是过于限制性的。两种方法都具有限制性,因此我们采用不同的做法,即提出一种检查子型的算法,这种算法是健全的,但不是完整的(在某些情况下,这种算法在不返回决定性判断的情况下终止了)。 算法基于一种树状,它代表着无节制子分立式的分型结构;这棵树可能是无限的,以及对于存在无限成功子树的有限证人进行算法检查。此外,我们提供了一种工具,用以执行我们的算法,我们用这个工具来检验它是否合理,我们用这个工具来检验我们以前的算法方法。 我们用这个工具来检验许多过去的例子,不能管理。