Manifest Sharing with Session Types
Manifest Sharing with Session Types
复制标题
DOI：
10.1145/3110281
复制
发表时间：
2017-09-01
影响因子：
1.8
通讯作者：
Pfenning, Frank
中科院分区：
文献类型：
--
作者：
Balzer, Stephanie;Pfenning, Frank
在线性逻辑和会话类型的通信保证会话忠诚度和僵局自由之间建立了咖喱 - 霍尔德同构的语言。不幸的是，这些强大的保证排除了许多与共享资源有关的自然存在的编程模式。在本文中，我们将共享介绍为会话类型的语言，其中类型被分层为线性和共享层，并与模态运算符连接这些层。由此产生的语言保留了会话保真度，而不是缺乏僵局，这可能是由于共享过程的争论而引起的。我们在各种示例（例如用餐哲学家问题）上说明了我们的语言，并将非同步pi-calculus的翻译转换为我们的语言。
Session-typed languages building on the Curry-Howard isomorphism between linear logic and session-typed communication guarantee session fidelity and deadlock freedom. Unfortunately, these strong guarantees exclude many naturally occurring programming patterns pertaining to shared resources. In this paper, we introduce sharing into a session-typed language where types are stratified into linear and shared layers with modal operators connecting the layers. The resulting language retains session fidelity but not the absence of deadlocks, which can arise from contention for shared processes. We illustrate our language on various examples, such as the dining philosophers problem, and provide a translation of the untyped asynchronous pi-calculus into our language.