一句话：提出πBI，用束蕴含逻辑解释会话类型，以spawn支持非线性资源共享，并证明类型保持、无死锁与弱规范化。
本文研究消息传递并发会话类型系统设计空间中的新位置。已有“命题即会话”对应多以线性逻辑为基础，资源必须线性消耗；作者转而采用 O’Hearn 与 Pym 的束蕴含逻辑（BI），将逻辑命题解释为并发进程类型，从而以全新方式处理非线性资源。论文引入带会话的 π 演算 πBI，其核心构造 spawn 表达由 BI 结构规则诱导的共享。作者给出基本理论：良类型进程的类型保持、无死锁与弱规范化；仿射 λ 演算的操作可靠且完备的类型编码；以及资源访问的非干涉结果，展示 πBI 的表达力。
The emergence of propositions-as-sessions, a Curry-Howard correspondence between propositions of Linear Logic and session types for concurrent processes, has settled the logical foundations of message-passing concurrency. Central to this approach is the resource consumption paradigm heralded by Linear Logic. In this paper, we investigate a new point in the design space of session type systems for message-passing concurrent programs. We identify O’Hearn and Pym’s Logic of Bunched Implications (BI) as a fruitful basis for an interpretation of the logic as a concurrent programming language. This leads to a treatment of non-linear resources that is radically different from existing approaches based on Linear Logic. We introduce a new π-calculus with sessions, called πBI; its most salient feature is a construct called spawn, which expresses new forms of sharing that are induced by structural principles in BI. We illustrate the expressiveness of πBI and lay out its fundamental theory: type preservation, deadlock-freedom, and weak normalization results for well-typed processes; an operationally sound and complete typed encoding of an affine λ-calculus; and a non-interference result for access of resources.
@article{paperbot1451,
title = {A bunch of sessions: a propositions-as-sessions interpretation of bunched implications in channel-based concurrency},
author = {Dan Frumin and Emanuele D’Osualdo and Bas van den Heuvel and Jorge A. Pérez},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563318}
}