论文标题
复制，重复使用，重复：通过会话类型和分级模态捕获非线性通信
Replicate, Reuse, Repeat: Capturing Non-Linear Communication via Session Types and Graded Modal Types
论文作者
论文摘要
会话类型提供了有关并发行为的保证，并且可以通过与线性逻辑的对应关系来理解，并将命题作为会话和证明作为过程。但是，严格的线性设置有些限制，因为存在依赖非线性行为的各种有用的通信模式。例如，共享频道提供了一种沿着新的线性会话型通道，反复带有二进制通信的过程。可以通过分级模态类型的一般概念以受控方式进行编程，这是一个包含各种系数键入的框架（描述计算如何在其上下文上提出需求）。本文展示了如何与会话类型一起利用分级的模态类型，以使各种非线性并发行为能够以线性为基础的类型系统以精确的方式重新引入。这里使用颗粒（一种具有线性，索引和分级模态类型的功能编程语言）来证明这里的想法。
Session types provide guarantees about concurrent behaviour and can be understood through their correspondence with linear logic, with propositions as sessions and proofs as processes. However, a strictly linear setting is somewhat limiting, since there exist various useful patterns of communication that rely on non-linear behaviours. For example, shared channels provide a way to repeatedly spawn a process with binary communication along a fresh linear session-typed channel. Non-linearity can be introduced in a controlled way in programming through the general concept of graded modal types, which are a framework encompassing various kinds of coeffect typing (describing how computations make demands on their context). This paper shows how graded modal types can be leveraged alongside session types to enable various non-linear concurrency behaviours to be re-introduced in a precise manner in a type system with a linear basis. The ideas here are demonstrated using Granule, a functional programming language with linear, indexed, and graded modal types.
