paperbot · PL 论文追踪

RSS

Interconnectability of Session-Based Logical Processes

TOPLAS 40(4)2018
Bernardo Toninho, Nobuko Yoshida

尚未生成 AI 速览(可能缺少 API key 或等待下次运行补跑)。

原文摘要(Abstract)

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.

链接与引用

DOI 原文 ·

BibTeX
@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}
}