Composition and decomposition of multiparty sessions
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.
scientific article; zbMATH DE number 7316060
scientific article