Composition and decomposition of multiparty sessions
type: Item
instance of: scholarly article
title: Composition and decomposition of multiparty sessions
zbMATH Open document ID: 1462.68120
author: Franco Barbanera
author: Ivan Lanese
author: Emilio Tuosto
author: Mariangiola Dezani-Ciancaglini
published in: Journal of Logical and Algebraic Methods in Programming
publication date: 2021-02-26T00:00:00Z
full work available at URL: OpenGTsynch-Main.pdf
review text: The authors look at multiparty sessions as open systems by allowing one to compose multiparty sessions by transforming two of their participants into a pair of coupled gateways, forwarding messages between the two sessions. It is shown that the session resulting from the composition can be typed, and its type can be computed from the global types of the starting sessions. As a consequence, lock-freedom is preserved by composition. Direct composition is also defined, which allows one to connect two global types without using gateways. Finally, a decomposition operator is proposed to split a global type into two, which is the left inverse of direct composition.
Mathematics Subject Classification ID: 68Q85
Mathematics Subject Classification ID: 68M14
zbMATH DE Number: 7316060
zbMATH Keywords: distributed systems
zbMATH Keywords: open systems
zbMATH Keywords: interface compatibility
MaRDI profile type: Publication
OpenAlex ID: W3094723157
cites work: Connecting open systems of communicating finite state machines
cites work: Reversible client/server interactions
cites work: Resolving Non-determinism in Choreographies
cites work: Q5129942
cites work: On Communicating Finite-State Machines
cites work: Undecidability of asynchronous session subtyping
cites work: Models, Languages, and Tools for Concurrent and Distributed Programming
cites work: Multiparty Session Types Within a Canonical Binary Theory, and Beyond
cites work: Q4608685
cites work: Q3077958
cites work: Reversible sessions with flexible choices
cites work: A Gentle Introduction to Multiparty Asynchronous Session Types
cites work: Global progress for dynamically interleaved multiparty sessions
cites work: Fundamental properties of infinite trees
cites work: Q2974797
cites work: Full Abstraction in a Subtyped pi-Calculus with Linear Types
cites work: Coordination Via Types in an Event-Based Framework
cites work: Subtyping Supports Safe Session Substitution
cites work: Subtyping for session types in the pi calculus
cites work: Precise subtyping for synchronous multiparty sessions
cites work: Multiparty asynchronous session types
cites work: Multiparty Asynchronous Session Types
cites work: A type system for lock-free processes
cites work: Practical coinduction
cites work: Synthesising Choreographies from Local Session Types
cites work: On the Undecidability of Asynchronous Session Subtyping
cites work: Global Principal Typing in Partially Commutative Asynchronous Sessions
cites work: Deadlock and lock freedom in the linear π-calculus
cites work: Types and programing languages
cites work: Q5019690
cites work: Observational Equivalence for Multiparty Sessions
DOI: 10.1016/J.JLAMP.2020.100620
description: scientific article; zbMATH DE number 7316060