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}$-模拟（也称为协变-逆变模拟），因此也推广了双模拟和普通模拟。我们进一步提出了一种子类型化算法，并证明了其可靠性，同时在编程语言编译器的背景下进行了实证评估。由于该算法所基于的模拟关系具有通用性，它也可能在其他领域找到应用。