具有无上下文会话类型的多态λ演算
摘要：无上下文会话类型提供了一种对双向通道上的递归结构化通信协议的类型约束。它们克服了常规会话类型系统仅适用于尾递归协议的限制。此扩展使我们能够以完全类型安全的方式实现树结构的序列化和反序列化。 我们介绍了语言FreeST 2的理论，该语言在具有线性类型和区分消息类型和通道类型的种类系统的System F扩展中引入了无上下文会话类型。该系统面临一些元理论挑战，其中包括在存在多态性的情况下的收缩性，类型上的非平凡等价理论以及类型等价的可判定性。我们还建立了类型保存、进展的标准结果以及对错误进程的特征描述。
作者：Bernardo Almeida, Andreia Mordido, Peter Thiemann, Vasco T. Vasconcelos
论文ID：2106.06658
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-08-03