子类型化的无上下文会话类型
摘要：无上下文会话类型描述在异构类型通道上的结构化通信模式，允许无尾递归约束的协议规范。然而，非规则递归提供了增强的表达能力，但以子类型的可决性为代价，即使等价性仍然可决。我们提出了一种基于一种新颖的观察预序$mathcal{XYZW}$-simulation的子类型上下文无关会话类型的方法，该方法泛化了$mathcal{XY}$-simulation（也称为协变-逆变模拟），因此也包括了等价模拟和普通模拟。我们进一步提出了一个我们证明是正确的子类型算法，并在一种编程语言的编译器环境下进行了实证评估。由于其建立在通用模拟关系之上的特点，该算法还可以在其他领域中找到应用。
作者：Gil Silva, Andreia Mordido and Vasco T. Vasconcelos
论文ID：2307.05661
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-07-13