Fair Subtyping for Open Session Types

Fair subtyping is a liveness-preserving refinement relation for session types akin to (but coarser than) the well-known should-testing precongruence. The behavioral characterization of fair subtyping is challenging essentially because fair subtyping is context-sensitive: two session types may or may not be related depending on the context in which they occur, hence the traditional coinductive argument for dealing with recursive types is unsound in general. In this paper we develop complete behavioral and axiomatic characterizations of fair subtyping and we give a polynomial algorithm to decide it.