  Multiparty session types (MPST) are a specification and verification
framework for distributed message-passing systems. The communication protocol
of the system is specified as a global type, from which a collection of local
types (local process implementations) is obtained by endpoint projection. A
global type is a single disciplining entity for the whole system, specified by
one designer that has full knowledge of the communication protocol. On the
other hand, distributed systems are often described in terms of their
components: a different designer is in charge of providing a subprotocol for
each component. The problem of modular specification of global protocols has
been addressed in the literature, but the state of the art focuses only on dual
input/output compatibility. Our work overcomes this limitation. We propose the
first MPST theory of multiparty compositionality for distributed protocol
specification that is semantics-preserving, allows the composition of two or
more components, and retains full MPST expressiveness. We introduce hybrid
types for describing subprotocols interacting with each other, define a novel
compatibility relation, explicitly describe an algorithm for composing multiple
subprotocols into a well-formed global type, and prove that compositionality
preserves projection, thus retaining semantic guarantees, such as liveness and
deadlock freedom. Finally, we test our work against real-world case studies and
we smoothly extend our novel compatibility to MPST with delegation and explicit
connections.
