Interconnection networks in session-based logical processes

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.