asynch-mpst-st

## Asynchronous Mutoparty Session Subtyping This archive contains a Coq mechanisation of subtyping for asynchronousmultiparty session types (MPSTs). The development formalises the theorypresented in: **Precise Subtyping for Asynchronous Multiparty Sessions** Ghilezan et al., *Journal of Logical and Algebraic Methods in Programming* (JLAMP), 2023, and its subsequent extension developed and mechanised in: **Completeness of Asynchronous Session Tree Subtyping in Coq** Ekici B. and Yoshida N., *International Conference on Interactive Theorem Proving* (ITP), 2024. An extended version of this mechanisation and its meta-theory is presented in anarticle submitted to *ACM Transactions on Computational Logic (TOCL)*. ### OverviewThe development formalises session trees, action reordering, refinement-basedsubtyping, and their meta-theoretic properties. It includes mechanised proofs ofcorrectness and completeness of asynchronous session subtyping, as well asverified examples drawn from the literature. ### ReproducibilityAll results are fully mechanised in Coq and can be reproduced by compiling thedevelopment. The artifact has been tested with Coq version 8.20.0.Detailed build instructions and a description of the repository structure areprovided in the README.md file. ### NotesThe formalisation makes essential use of coinductive definitions and employsclassical reasoning in selected proofs, as discussed in the accompanying papers.