Subtyping recursive types
Résumé
We investigate the interactions of subtyping and recursive types, in a simply typed lambda-calculus. The two fundamental questions here are whether two (recursive) types are in the subtype relation, and whether a term has a type.