Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection
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 \emph{global type}, from which a collection of \emph{local types} (local process implementations) is obtained by \emph{endpoint projection}. A global type is a single disciplining entity for the whole system, specified by \emph{one designer} that has full knowledge of the communication protocol. On the other hand, distributed systems are often described in terms of their \emph{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 \emph{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 \emph{hybrid types} for describing subprotocols interacting with each other, define a novel \emph{compatibility relation}, explicitly describe an algorithm for composing multiple subprotocols into a \emph{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.