论文标题
会话类型的多态性典型型
Polymorphic Typestate for Session Types
论文作者
论文摘要
会话类型为打字的通信协议提供了一种原则性的方法，该协议可以保证类型安全和协议保真度。会话类型的通信的形式化通常基于过程计算，并发lambda calculi或线性逻辑。基于上下文敏感的键入和典型的替代模型由于其明显的限制并没有得到太多关注。但是，该模型很有吸引力，因为它不会迫使程序员进入诸如持续通行的样式或通道风格之类的特定模式，而是使他们能够像可变变量一样对待通信渠道。多态性典型是可以对会话类型的沟通进行全面处理的关键。以前朝这个方向的工作受到了简单型的lambda演算的限制。我们表明，高阶多态性和存在类型使我们能够取消以前的作品施加的限制，从而使基于典型的方法的表达性与竞争相同。在此基础上，我们定义了PolyVgr，即用于会话类型的多态性类型系统，建立其基本的元看，类型保存和进度，并提供原型实现。
Session types provide a principled approach to typed communication protocols that guarantee type safety and protocol fidelity. Formalizations of session-typed communication are typically based on process calculi, concurrent lambda calculi, or linear logic. An alternative model based on context-sensitive typing and typestate has not received much attention due to its apparent restrictions. However, this model is attractive because it does not force programmers into particular patterns like continuation-passing style or channel-passing style, but rather enables them to treat communication channels like mutable variables. Polymorphic typestate is the key that enables a full treatment of session-typed communication. Previous work in this direction was hampered by its setting in a simply-typed lambda calculus. We show that higher-order polymorphism and existential types enable us to lift the restrictions imposed by the previous work, thus bringing the expressivity of the typestate-based approach on par with the competition. On this basis, we define PolyVGR, the system of polymorphic typestate for session types, establish its basic metatheory, type preservation and progress, and present a prototype implementation.
