Multiparty session types (MPST) serve as a foundational framework for formally specifying and verifying message-passing protocols. Asynchronous subtyping in MPST allows for typing optimised programs preserving type safety and deadlock freedom under asynchronous interactions where the order of messages sent (resp. received) to (resp. from) particular participant is preserved and sending is non-blocking. The optimisation is achieved by reordering send actions with any other action, except sends to the same participant, and by reordering receive actions with other receive actions, except those from the same participant. Sound subtyping algorithms have been extensively studied and implemented as part of various programming languages and tools including C, Rust and C-MPI. However, formalising all such permutations under sequencing, selection, branching and recursion in session types is an intricate task. Additionally, checking asynchronous subtyping has been proven to be undecidable. This article presents the first formalisation of asynchronous subtyping for MPST within the Coq proof assistant. We begin by translating session types into session trees , unfolding recursion coinductively. These trees are then decomposed into new tree forms that incorporate singleton branching and/or selection constructs. On these trees, which involve both singleton branching and selections, we define action reorderings within a coinductive refinement relation that governs subtyping. To demonstrate the expressiveness of our formalisation, we verify several subtyping schemas drawn from the literature—none of which can be simultaneously validated by existing decidable but sound algorithms. Additionally, we take the (inductive) negation of the refinement relation from a prior work by Ghilezan et al. and re-implement it, significantly reducing the number of rules (from eighteen to eight). We establish the completeness of subtyping with respect to its negation in Coq. We establish the correctness of the refinement relation, in Coq, showing that it preserves the ordering of send (resp. receive) actions to (resp. from) a specific participant. Additionally, we formally demonstrate in Coq that refinement is transitive, a property crucial for closing certain cases in subtyping proofs. In the formalisation, we use the greatest fixed point of the least fixed point technique, facilitated by the Paco library, to define coinductive predicates. We employ parametrised coinduction to prove their properties. The formalisation consists of roughly 32K lines of Coq code and is available on GitHub at https://github.com/ekiciburak/async-mpst-st/tree/acm and on Zenodo at https://doi.org/10.5281/zenodo.18268293 .

Multiparty session types (MPST) provide a robust typing discipline for specifying and verifying communication protocols in concurrent and distributed systems involving multiple participants. This work formalises the non-stuck theorem for synchronous MPST in the Coq proof assistant, ensuring that well-typed communications never get stuck. We present a fully mechanised proof of the theorem, where recursive type unfoldings are modelled as infinite trees, leveraging coinductive reasoning. This marks the first formal proof to incorporate precise subtyping, aiming to extend the typability of processes thus precision of the type system. The proof is grounded in fundamental properties such as subject reduction and progress. During the mechanisation process, we discovered that the structural congruence rule for recursive processes, as presented in several prior works on MPST, violates subject reduction. We resolve this issue by revising and formalising the rule to ensure the preservation of type soundness. Our approach to formal proofs about infinite type trees involves analysing their finite prefixes through inductive reasoning within outer-level coinductively stated goals. We employ the greatest fixed point of the parameterised least fixed point technique to define coinductive predicates and use parameterised coinduction to prove properties. The formalisation comprises approximately 16K lines of Coq code, accessible at: https://github.com/Apiros3/smpst-sr-smer.