论文标题
嵌套会话类型
Nested Session Types
论文作者
论文摘要
会话类型静态地描述并发通信过程之间的通信协议。不幸的是，在会话类型的背景下，即使以限制性的prenex形式也无法完全理解参数多态性。在本文中，我们介绍了与prenex多态性扩展的会话类型的元理性，结果是嵌套的递归数据类型。值得注意的是，我们通过表现出降低以追踪确定性一阶语法的等效性来确定类型平等。认识到后者的高理论复杂性，我们还提出了一种新型类型的平等算法并证明其健全性。我们观察到该算法效率非常高，尽管它不完整，但对于我们的所有示例都足够。我们通过将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 paper, 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.
