论文标题
一系列会议：基于渠道并发的构成含义的命题 - 按课程解释
A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency
论文作者
论文摘要
命题 - 按课程的出现，即线性逻辑的命题和会话类型之间的咖喱途径对应关系，为并发过程解决了会议类型，已解决了消息传递并发的逻辑基础。这种方法的核心是线性逻辑预示的资源消费范式。 在本文中，我们研究了会话类型系统的设计空间中的一个新点，以通过消息引起并发程序。我们将O'Hearn和Pym的束缚含义（BI）逻辑确定为将逻辑解释为并发编程语言的富有成效的基础。这导致对非线性资源的处理与基于线性逻辑的现有方法根本不同。我们引入了一个带有会话的新的$π$ -calculus，称为$π$ bi;它最突出的特征是一种称为Spawn的构造，它表达了由BI中结构原理引起的新形式的共享形式。我们说明了$π$ bi的表现力，并列出了其基本理论：类型保存，僵局 - 自由和较弱的过程的正常化结果；仿射$λ$ -calculus的操作声音和完整的键入编码；以及访问资源的非干预结果。
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.
