A List of Successes That Can Change the World
A List of Successes That Can Change the World
复制标题
可以改变世界的成功清单
DOI：
10.1007/978-3-319-30936-1_2
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Atkey R
中科院分区：
文献类型：
--
作者：
Atkey R
会话类型提供了并发程序遵守通信协议的静态保证。最近的工作探索了证明规则和削减减少线性逻辑和过程演算的类型和评价之间的对应关系。本文考虑了两种方法来扩展逻辑建立的进程演算。首先，我们考虑扩展的过程演算更密切的竞争演算。其次，受进程演算的指称模型的启发，我们考虑合并对偶类型。最有趣的是，我们观察到，这些方法是一致的：合并乘法（和$$\invamp $$）允许进程共享多个通道;合并加法（和）提供不确定性;合并指数（和）产生接入点，用于启动会话类型通信的会合机制。访问点特别有表现力：例如，它们足以对并发状态和一般递归进行编码。
Session types provide a static guarantee that concurrent programs respect communication protocols. Recent work has explored a correspondence between proof rules and cut reduction in linear logic and typing and evaluation of process calculi. This paper considers two approaches to extend logically-founded process calculi. First, we consider extensions of the process calculus to more closely resemble-calculus. Second, inspired by denotational models of process calculi, we consider conflating dual types. Most interestingly, we observe that these approaches coincide: conflating the multiplicatives (and $$\invamp $$) allows processes to share multiple channels; conflating the additives (and) provides nondeterminism; and conflating the exponentials (and) yields access points, a rendezvous mechanism for initiating session typed communication. Access points are particularly expressive: for example, they are sufficient to encode concurrent state and general recursion.