Polarized Substructural Session Types
Polarized Substructural Session Types
复制标题
极化的底层会话类型
DOI：
10.1007/978-3-662-46678-0_1
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Dennis Griffith
中科院分区：
文献类型：
--
作者：
F. Pfenning;Dennis Griffith
会话类型的并发和线性逻辑之间的深厚连接体现在集成功能和消息的并发编程的语言基础上。线性打字的严格性质提供了强大的保证，例如全球进步，缺席的僵局和种族自由，但它也需要程序员明确的资源管理。这种负担在仿射类型系统中减轻了不需要使用资源的简单形式的垃圾收集。
The deep connection between session-typed concurrency and linear logic is embodied in the language SILL that integrates functional and message-passing concurrent programming. The exacting nature of linear typing provides strong guarantees, such as global progress, absence of deadlock, and race freedom, but it also requires explicit resource management by the programmer. This burden is alleviated in an affine type system where resources need not be used, relying on a simple form of garbage collection.