多态类型状态用于会话类型
摘要：多态类型状态：基于会话类型的多态类型状态系统 会话类型提供了一种有原则的方法来保证类型安全和协议的完整性的类型化通信协议。对于会话类型的形式化通信，通常基于进程演算、并发λ演算或线性逻辑。基于上下文敏感类型和类型状态的另一种模型因其表面上的限制而未受到广泛关注。然而，这个模型很有吸引力，因为它不强制程序员采用特定的模式，如持续传递风格或通道传递风格，而是使他们能够像处理可变变量一样处理通信通道。多态类型状态是使会话类型通信得到完整处理的关键。先前的工作因在简单类型λ演算中进行而受到限制。我们展示了高阶多态性和存在类型使我们能够解除先前工作所施加的限制，从而使基于类型状态的方法的表达能力与竞争者相当。在此基础上，我们定义了PolyVGR，一种用于会话类型的多态类型状态系统，并建立了其基本元理论、类型保持性和进展性，并提出了一个原型实现。
作者：Hannes Saffrich and Peter Thiemann
论文ID：2210.17335
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-08-15