Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper introduces a denotational semantics for asynchronous multiparty session types with asynchronous subtyping, enabling formal reasoning about asynchronous message-passing and communication optimizations like message reordering. The semantics models message-passing as a computational effect, leveraging grading to track these effects and connect multiparty session typing to grading paradigms. The utility of the model is demonstrated by proving it adequate for a call-by-value calculus, ensuring communication safety, deadlock-freedom, and liveness even with communication optimizations.
Asynchronous multiparty session types finally get a denotational semantics, unlocking formal verification of message reordering and other communication optimizations.
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.