一句话：证明经典线性逻辑的会话式进程组合在互连网络上弱于多党会话演算，并提出保持无死锁的循环互连组合规则。
在多党会话类型中，互连网络用于刻画会话角色之间的通信连接；而在经典线性逻辑（CLL）的会话式进程解释中，相应问题是什么进程可通过兼容通道进行组合（cut）。本文比较这两种框架的互连表达能力。为建立比较，作者提出部分多党兼容性（PMC）这一组合式综合性质，用以从良类型 CLL 线程的迭代组合构造全局类型。结果表明，CLL 组合诱导的 PMC 全局类型不允许三个及以上参与者之间的循环互连，因此其互连网络严格弱于多党会话演算。最后，论文利用 PMC 定义了一条新的 CLL 组合规则，使其能够形成循环互连，同时保持 CLL 的无死锁性。
In multiparty session types, interconnection networks identify which roles in a session engage in communication (i.e., two roles are connected if they exchange a message). In session-based interpretations of linear logic the analogue notion corresponds to determining which processes are composed, or cut, using compatible channels typed by linear propositions. In this work, we show that well-formed interactions represented in a session-based interpretation of classical linear logic (CLL) form strictly less-expressive interconnection networks than those of a multiparty session calculus. To achieve this result, we introduce a new compositional synthesis property dubbed partial multiparty compatibility (PMC), enabling us to build a global type denoting the interactions obtained by iterated composition of well-typed CLL threads. We then show that CLL composition induces PMC global types without circular interconnections between three (or more) participants. PMC is then used to define a new CLL composition rule that can form circular interconnections but preserves the deadlock-freedom of CLL.
@article{paperbot308,
title = {Interconnectability of Session-Based Logical Processes},
author = {Bernardo Toninho and Nobuko Yoshida},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {40},
number = {4},
year = {2018},
doi = {10.1145/3242173}
}