| Summary: | 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 message order is preserved and sending is non-blocking. The optimisation is obtained by
message reordering, which allows for sending messages earlier or receiving them later. 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 introduces the first formalisation of asynchronous subtyping in MPST within the Coq
proof assistant. We first decompose session types into session trees that do not involve branching
and selection, and then establish a coinductive refinement relation over them to govern subtyping.
To showcase our formalisation, we prove example subtyping schemas that appear in the literature,
all of which cannot be verified, at the same time, by any of the existing decidable sound algorithms.
Additionally, we take the (inductive) negation of the refinement relation from a prior work by
Ghilezan et al. [21] 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, addressing
the issues concerning the negation rules outlined in the previous work [21].
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 10K lin
|
|---|