Abstract: We discuss some of the proposals in the literature about contract theories and session  types dealing with asynchronous communication. Assuming that communication is mediated by buffers, notions of compatibility, contract refinement and session subtyping can be defined that are less restrictive w.r.t. their synchronous counterparts. Unfortunately,  most of such notions in the literature turn out to be undecidable. We discuss the source of this negative result, and present some proposals to overcome this limitation, with the aim of obtaining algorithmic versions of such notions.

The content in these slides was presented during the BehAPI 2019 Summer School in Leicester.