Sciweavers

TACS
1991
Springer

An Extension of System F with Subtyping

13 years 7 months ago
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. Appears in: International Conference on Theoretical Aspects of Computer Software, T.Ito, A.R.Meyer Eds., Lecture
Luca Cardelli, Simone Martini, John C. Mitchell, A
Added 27 Aug 2010
Updated 27 Aug 2010
Type Conference
Year 1991
Where TACS
Authors Luca Cardelli, Simone Martini, John C. Mitchell, Andre Scedrov
Comments (0)