Undecidability of Asynchronous Session Subtyping: the Hunt for Significant Decidable Variants

Session types are behavioural types for guaranteeing that concurrent programs are free from basic communication errors. We recently proved that, differently from what previously claimed, the notion of asynchronous subtyping for session types is undecidable. This opened up, in the session type research community, the problem of finding possible variants that make such relation decidable. It is indeed important to reason about significant cases, having some impact in practical applications of session types, and develop the corresponding subtyping algorithms. This because, e.g., session types have become popular in mainstream programming languages, and, in this context, asynchronous communications are the norm rather than the exception.