Asynchronous multiparty session types are a type-based framework which ensure the compatibility of components in a distributed system by checking compliance against a specified global protocol. We propose a top-down approach, starting with the global protocol which is then projected into a set of local specifications. Next, we use an asynchronous refinement relation, precise asynchronous multiparty subtyping, to enable local specifications to be optimised by permuting actions within individual asynchronous components. This supports local reasoning, as each component can be independently developed and refined in isolation, before being integrated into a larger system. We show that this methodology guarantees both type soundness and liveness of the collection of optimised components. In this article, we first propose new operational semantics of global protocols which capture sound optimisations in the context of asynchronous message-passing. Next we define an asynchronous association between global protocols and a set of optimised local types. Thirdly, we prove, for the first time, the correctness of the most expressive endpoint projection in the literature, coinductive full merging projection. We then show the main theorems of this article: soundness and completeness of the operational correspondence of the asynchronous association. As a consequence, the association acts as an invariant that can be used to transfer key theorems from the bottom-up system to the top-down system. In particular, we used this to prove type soundness, session-fidelity, deadlock-freedom and liveness of the collection of optimised endpoints.

翻译：异步多方会话类型是一种基于类型的框架，通过检查分布式系统中各组件是否符合指定的全局协议来确保其兼容性。我们提出一种自上而下的方法：从全局协议出发，将其投影为一组本地规约；随后采用异步精化关系——精确异步多方子类型——通过调整单个异步组件内部的动作顺序来实现本地规约的优化。这种方法支持本地化推理，允许每个组件在集成到更大系统之前独立开发和精化。我们证明该方法能同时保证优化后组件集合的类型可靠性和活性。本文首先提出了全局协议的新操作语义，以捕捉异步消息传递语境下的可靠优化；其次定义了全局协议与优化后本地类型集合间的异步关联关系；第三，首次证明了文献中最具表达力的端点投影方法——共归纳完全合并投影——的正确性。随后我们展示了本文的核心定理：异步关联关系操作对应性的可靠性与完备性。由此，该关联关系可作为不变量，用于将自底向上系统中的关键定理迁移至自顶向下系统。特别地，我们运用此方法证明了优化后端点集合的类型可靠性、会话保真性、无死锁性及活性。