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.

翻译：多元会话类型（MPST）是一种用于分布式消息传递系统的规范与验证框架。系统的通信协议被指定为全局类型，通过端点投影可从中获得一组局部类型（局部进程实现）。全局类型是整个系统的单一规约实体，由完全了解通信协议的设计者指定。另一方面，分布式系统通常按其组件进行描述：不同设计者负责为每个组件提供子协议。全局协议的模块化规约问题已在文献中得到探讨，但现有研究仅关注二元输入/输出兼容性。我们的工作突破了这一局限。我们首次提出了一种保持语义的、支持两个及以上组件组合、并保留完整MPST表达能力的分布式协议规约多元组合性MPST理论。我们引入了用于描述相互交互的子协议的混合类型，定义了新型兼容性关系，明确描述了将多个子协议组合成良构全局类型的算法，并证明了组合性保持投影性质，从而保留活性与无死锁等语义保证。最后，我们通过真实案例研究验证了所提方法，并将新型兼容性平滑扩展至包含委托与显式连接的MPST。