Primitive subtyping /\ implicit polymorphism |= object-orientation

We present a new predicative and decidable type system, called ML-sub that adds primitive subtyping to the ML type system. Our goal is to devise a type discipline for a strongly typed, higher-order object-oriented language, building on well-understood concepts from type systems for functional languages, rather than on special calculi or resorting to "ad-hoc" polymorphism, second-order systems, or recursive types.

[PostScript, PDF, Software]

François Bourdoncle