We provide the first denotational semantics for asynchronous multiparty session types with precise asynchronous subtyping. Our semantics enables us to reason about asynchronous message-passing, in which message-sending is non-blocking. It enables us to prove the correctness of communication optimisations, in particular, those involving reordering of messages. Our development crucially relies on modelling message-passing as a computational effect. We apply grading, a paradigm for tracking computational effects, to asynchronous message-passing, demonstrating that multiparty session typing can be viewed as an instance of grading. We demonstrate the utility of our model by showing that it forms an adequate denotational semantics for a call-by-value asynchronous message-passing calculus, that ensures communication safety, deadlock-freedom and liveness in the presence of communication optimisations.

翻译：我们首次为具有精确异步子类型的异步多参与者会话类型建立了指称语义。该语义使我们能够对消息发送非阻塞的异步消息传递进行推理，并能够证明通信优化的正确性，特别是涉及消息重排的优化。我们的关键进展在于将消息传递建模为一种计算效应。我们应用分级法（一种追踪计算效应的范式）来处理异步消息传递，表明多参与者会话类型可视为分级法的一个实例。通过证明该模型构成了按值调用异步消息传递演算的恰当指称语义（确保通信安全性、无死锁性以及通信优化存在下的活跃性），我们展示了其效用。