Inference Systems with Corules for Fair Subtyping and Liveness Properties of Binary Session Types