π-calculus, Session Types research at the University of Oxford
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 paper presents the first formalisation of asynchronous subtyping for multiparty session types 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.
@article{EY2026,
author = {Burak Ekici and Nobuko Yoshida},
title = {{Formalising Asynchronous Session Subtyping}},
journal = {ACM-TOCL},
pages = {--},
publisher = {ACM},
year = 2026
}
@article{EY2026,
author = {Burak Ekici and Nobuko Yoshida},
title = {{Formalising Asynchronous Session Subtyping}},
journal = {ACM Transactions on Computational Logic},
pages = {--},
publisher = {ACM},
year = 2026
}