一句话：基于伴随逻辑的类型论统一编码 future、fork/join 与单子并发，并给出线性 future 的形式化基础。
常见并发语言通常从顺序语言出发，再添加对并发访问有限制的构造（如 future），虽成功但缺乏令人满意的理论基础，且难以同时使用多种并发构造。本文反向而行：以伴随逻辑（adjoint logic）的 Curry–Howard 解释为基础构造并发语言，加入三个原子原语以编码顺序组合和各种同步。该语言表达力强，可在同一框架中编码 future、fork/join 并行与单子并发；借助伴随逻辑，还能为 Blelloch 和 Reid-Miller 在复杂度分析中使用的线性 future 给出形式化说明。方法的统一性使得许多并发原语可以线性方式处理，并允许在同一程序中混合多种并发形式。
Abstract Common approaches to concurrent programming begin with languages whose semantics are naturally sequential and add new constructs that provide limited access to concurrency, as exemplified by futures . This approach has been quite successful, but often does not provide a satisfactory theoretical backing for the concurrency constructs, and it can be difficult to give a good semantics that allows a programmer to use more than one of these constructs at a time. We take a different approach, starting with a concurrent language based on a Curry–Howard interpretation of adjoint logic, to which we add three atomic primitives that allow us to encode sequential composition and various forms of synchronization. The resulting language is highly expressive, allowing us to encode futures, fork/join parallelism, and monadic concurrency in the same framework. Notably, since our language is based on adjoint logic, we are able to give a formal account of linear futures , which have been used in complexity analysis by Blelloch and Reid-Miller. The uniformity of this approach means that we can similarly work with many of the other concurrency primitives in a linear fashion, and that we can mix several of these forms of concurrency in the same program to serve different purposes.