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.

翻译：异步多方会话类型是一种基于类型的框架，通过检查对指定全局协议的遵循性，确保分布式系统中组件的兼容性。我们提出一种自顶向下的方法，从全局协议开始，将其投影为一组局部规范。接着，利用一种异步精化关系——精确异步多方子类型化——通过重排单个异步组件内的动作顺序，实现对局部规范的优化。这种方法支持局部推理，因为每个组件可在集成到更大系统前独立开发与隔离精化。我们证明，该方法论能保证优化后组件集合的类型安全性及活性。本文首先提出捕捉异步消息传递中有效优化的全局协议新操作语义，其次定义全局协议与一组优化局部类型之间的异步关联，再次首次证明文献中最具表达力的端点投影——共归纳全合并投影——的正确性，随后展示本文主要定理：异步关联的操作对应性的可靠性与完备性。该关联作为不变量，可用于将自底向上系统中的关键定理迁移至自顶向下系统。特别地，我们利用它证明了优化端点集合的类型安全性、会话保真性、无死锁性及活性。