Interconnectability of session-based logical processes
File(s)
Published version
Author(s)
Toninho, B
Yoshida, N
Type
Journal Article
Abstract
In multiparty session types, interconnection networks identify which roles in a session engage in communica-tion (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 which can form circular interconnections but preserves the deadlock-freedom of CLL.
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 which can form circular interconnections but preserves the deadlock-freedom of CLL.
Date Issued
2018-12-01
Date Acceptance
2018-07-25
Citation
ACM Transactions on Programming Languages and Systems, 2018, 40 (4)
ISSN
0164-0925
Publisher
Association for Computing Machinery
Journal / Book Title
ACM Transactions on Programming Languages and Systems
Volume
40
Issue
4
Copyright Statement
© 2018 Copyright is held by the owner/author(s). Publication rights licensed to ACM. This work is licensed under a Creative Commons Attribution International 4.0 License (https://creativecommons.org/licenses/by/4.0/)
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Grant Number
ERI 025567 (EP/K034413/1)
PO 20015393
EP/K011715/1
EP/N027833/1
PO 20015391
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science
Session types
classical linear logic
multiparty sessions
synthesis
PI-CALCULUS
MULTIPARTY
VERIFICATION
0803 Computer Software
0806 Information Systems
Software Engineering
Publication Status
Published
Article Number
ARTN 17