Interconnection networks in session-based logical processes
File(s)DTRS16-5.pdf (506 KB)
Published version
Author(s)
Toninho, Bernardo
Yoshida, Nobuko
Type
Report
Abstract
In multiparty session types, interconnection networks identify
which roles in a session engage in direct communication. If role
p is connected to role q, then p exchanges a message with q.
In a session-based interpretation of classical linear logic (CLL),
this corresponds to the composition, or cut, of dual propositions.
This paper shows that well-formed interactions represented in a
session-based interpretation of CLL form strictly less expressive
interconnection networks than those specified in a multiparty session
calculus. To achieve this, 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 processes.We show that
the CLL composition rule induces PMC global types without circular
interconnections between three participants. PMC is then used
to define a new CLL multicut rule which can form general multiparty
interconnections, preserving the deadlock-freedom property
of CLL.
which roles in a session engage in direct communication. If role
p is connected to role q, then p exchanges a message with q.
In a session-based interpretation of classical linear logic (CLL),
this corresponds to the composition, or cut, of dual propositions.
This paper shows that well-formed interactions represented in a
session-based interpretation of CLL form strictly less expressive
interconnection networks than those specified in a multiparty session
calculus. To achieve this, 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 processes.We show that
the CLL composition rule induces PMC global types without circular
interconnections between three participants. PMC is then used
to define a new CLL multicut rule which can form general multiparty
interconnections, preserving the deadlock-freedom property
of CLL.
Date Issued
2016-01-01
Citation
Departmental Technical Report: 16/5, 2016, pp.1-18
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
18
Journal / Book Title
Departmental Technical Report: 16/5
Copyright Statement
© 2016 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
16/5