An Extension of System F with Subtyping

AbstractSystem 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 proof-theoretical 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