An extension of system F with subtyping

System F is a well-known typed λ-calculus with polymorphic types, which provides a basis for polymorphic programming languages. We study an extension of F, called F <: (pronounced ef-sub) that combines parametric polymorphism with subtyping. The main focus of the paper is the equational theory of F <: , which is related to PER models and the notion of parametricity. We study some categorical properties of the theory when restricted to closed terms, including interesting categorical isomorphisms. We also investigate prooftheoretical properties, such as the conservativity of typing judgments with respect to F. We demonstrate by a set of examples how a range of constructs may be encoded in F <:. These include record operations and subtyping hierarchies that are related to features of object-oriented languages