Skip to Main content Skip to Navigation
Journal articles

Composition and Decomposition of Multiparty Sessions

Abstract : Multiparty sessions are systems of concurrent processes, which allow several participants to communicate by sending and receiving messages. Their overall behaviour can be described by means of global types. Typable multiparty sessions enjoy lock-freedom. We 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. Gateways need to be compatible. We show 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. Compatibility between global types is necessary, since systems obtained by composing sessions with incompatible global types have locks (or they are not sessions). We also define direct composition, which allows one to connect two global types without using gateways. Finally, we propose a decomposition operator, to split a global type into two, which is the left inverse of direct composition. Direct composition and decomposition on global types prepare the ground for a novel framework allowing for the modular design and implementation of distributed systems.
Complete list of metadata
Contributor : Ivan Lanese Connect in order to contact the contributor
Submitted on : Thursday, September 9, 2021 - 12:19:57 AM
Last modification on : Friday, July 8, 2022 - 10:06:04 AM
Long-term archiving on: : Friday, December 10, 2021 - 6:10:06 PM


Files produced by the author(s)




Franco Barbanera, Mariangiola Dezani-Ciancaglini, Ivan Lanese, Emilio Tuosto. Composition and Decomposition of Multiparty Sessions. Journal of Logical and Algebraic Methods in Programming, Elsevier, 2021, ⟨10.1016/j.jlamp.2020.100620⟩. ⟨hal-03338671⟩



Record views


Files downloads