Session types for asynchronous communication: a new subtyping and its implementation

Session types are a promising way to describe communication protocols directly through the type system, allowing to check the correctness of a system at compile time. This thesis represents a study of session subtyping, i.e., the substitutability of components, starting from the work by Bravetti, Lange, and Zavattaro, who presented a definition of fair asynchronous subtyping. Their subtyping allows the anticipation of messages emissions without the restrictions imposed by previous results on this field. Since covariance of outputs is not allowed by the original version of subtyping, we tried to address this problem and to introduce covariance into the original proposal of fair asynchronous subtyping. Finally, we describe the integration process of the new definition of subtyping within the tool for the check of subtyping relation.