AN EXTENSION OF SYSTEM-F WITH SUBTYPING

System F is a well-known typed lambda-calculus with polymorphic types, which provides a basis for polymorphic programming languages. We stud y an extension of F, called F<: (pronounced ef-sub), that combines par ametric polymorphism with subtyping. The main focus of the paper is th e equational theory of F<:, which is related to PER models and the not ion of parametricity. We study some categorical properties of the theo ry when restricted to closed terms, including interesting categorical isomorphisms. We also investigate proof-theoretical properties, such a s the conservativity of typing judgments with respect to F We demonstr ate 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. (C) 1994 Academic P ress, Inc.