一句话：为会话类型引入 prenex 多态与嵌套递归数据类型，证明类型等价可判定并提出高效可靠算法。
会话类型可静态描述并发消息传递进程之间的通信协议，但即使在受限的 prenex 形式下，参数多态在会话类型中的理论仍未被充分理解。本文给出扩展 prenex 多态的会话类型元理论，并由此支持嵌套递归数据类型。作者证明类型等价是可判定的，方法是将该问题归约为确定性一阶文法的 trace equivalence；鉴于该归约的理论复杂度较高，又提出一种新的类型等价算法并证明其可靠性。该算法虽不完备，但作者观察到其效率出奇地高，且足以处理论文中的所有例子。作者通过扩展 Rast 编程语言实现这些思想，并用若干示例展示增强后类型系统的表达力。
Session types statically describe communication protocols between concurrent message-passing processes. Unfortunately, parametric polymorphism even in its restricted prenex form is not fully understood in the context of session types. In this article, we present the metatheory of session types extended with prenex polymorphism and, as a result, nested recursive datatypes. Remarkably, we prove that type equality is decidable by exhibiting a reduction to trace equivalence of deterministic first-order grammars. Recognizing the high theoretical complexity of the latter, we also propose a novel type equality algorithm and prove its soundness. We observe that the algorithm is surprisingly efficient and, despite its incompleteness, sufficient for all our examples. We have implemented our ideas by extending the Rast programming language with nested session types. We conclude with several examples illustrating the expressivity of our enhanced type system.
@article{paperbot1612,
title = {Nested Session Types},
author = {Ankush Das and Henry Deyoung and Andreia Mordido and Frank Pfenning},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {44},
number = {3},
year = {2022},
doi = {10.1145/3539656}
}