论文标题
会话类型带有算术改进
Session Types with Arithmetic Refinements
论文作者
论文摘要
会话类型在静态规定消息通信过程的双向通信协议上。但是，简单的会话类型无法指定超出交换消息类型之外的属性。在本文中，我们通过使用线性算术捕获数据结构和算法的内在属性的索引修补来扩展类型系统。我们表明，尽管Presburger算术具有可决定性，但类型相等，因此现在不可确定，这是不可决定的，这与功能性语言的类似依赖性细化类型系统形成了鲜明对比。我们还提出了一种实用但不完整的类型平等算法，我们在实施RAST时使用了这种算法，这是一种同时进行的会话类型的语言，具有算术索引修补，以及测量和时间类型。此外，如有必要，程序员可以提出其他类型的仿真，这些型号平滑地集成到类型相等算法中。
Session types statically prescribe bidirectional communication protocols for message-passing processes. However, simple session types cannot specify properties beyond the type of exchanged messages. In this paper we extend the type system by using index refinements from linear arithmetic capturing intrinsic attributes of data structures and algorithms. We show that, despite the decidability of Presburger arithmetic, type equality and therefore also subtyping and type checking are now undecidable, which stands in contrast to analogous dependent refinement type systems from functional languages. We also present a practical, but incomplete algorithm for type equality, which we have used in our implementation of Rast, a concurrent session-typed language with arithmetic index refinements as well as ergometric and temporal types. Moreover, if necessary, the programmer can propose additional type bisimulations that are smoothly integrated into the type equality algorithm.
