Context-free session types describe structured patterns of communication on heterogeneously-typed channels, allowing the specification of protocols unconstrained by tail recursion. The enhanced expressive power provided by non-regular recursion comes, however, at the cost of the decidability of subtyping, even if equivalence is still decidable. We present an approach to subtyping context-free session types based on a novel kind of observational preorder we call $\mathcal{XYZW}$-simulation, which generalizes $\mathcal{XY}$-simulation (also known as covariant-contravariant simulation) and therefore also bisimulation and plain simulation. We further propose a subtyping algorithm that we prove to be sound, and present an empirical evaluation in the context of a compiler for a programming language. Due to the general nature of the simulation relation upon which it is built, this algorithm may also find applications in other domains.

翻译：上下文无关会话语境类型描述了异构类型通道上的结构化通信模式，允许指定不受尾递归约束的协议。然而，非正则递归提供的增强表达能力以子类型化可判定性为代价，即便等价性仍可判定。我们提出了一种基于新型观测预序（称为$\mathcal{XYZW}$-模拟）的子类型化上下文无关会话语境类型方法，该方法推广了$\mathcal{XY}$-模拟（也称为协变-逆变模拟），进而也推广了互模拟和普通模拟。我们进一步提出了一种子类型化算法并证明其可靠性，并在编程语言编译器的背景下进行了实证评估。由于其所基于的模拟关系具有通用性，该算法也可能在其他领域找到应用。