A symbolic labelled transition system for coinductive subtyping of Fμ⩽ types

F_⩽ is a typed λ-calculus with subtyping and bounded polymorphism. Type checking for F_⩽ is known to be undecidable, because the subtyping relation on types is undecidable. F _μ⩽ is an extension of F_⩽ with recursive types. In this paper, we show how symbolic labelled transition system techniques from concurrency theory can be used to reason about subtyping for F_μ⩽. We provide a symbolic labelled transition system for F_μ⩽ types, together with an appropriate notion of simulation, which coincides with the existing co-inductive definition of subtyping. We then provide a `simulation up to´ technique for proving subtyping, for which there is a simple model-checking algorithm. The algorithm is more powerful than the usual one for F_⩽, e.g. it terminates on G. Ghelli´s (1995) canonical example of non-termination