This thesis develops a sound type system for a model object-oriented language that addresses this lack of flexibility. It separates the notions of subtyping and inheritance, producing a more flexible language. It also supports method specialization, which means that the types of methods may be specialized in certain ways during inheritance. The lack of such a mechanism is one of the key sources of type casts in languages like C++ and Object Pascal. The thesis then extends this core object calculus with abstraction primitives that support a class construct similar to the one found in languages such as C++, Eiffel, and Java. This formal study explains the link between inheritance and subtyping: object types that include implementation information are a form of abstract type, and the only way to get a subtype of an abstract type is by extension (i.e., by inheritance). The study also suggests that object primitives and encapsulation are orthogonal language features that together produce object-oriented programming. Hence, adding object primitives to a language that already supports encapsulation (such as ML) should be sufficient to create an object-oriented language.
Formally, the language is presented as an object calculus and a type system with row variables, variance annotations, method absence annotations, and abstract types. The thesis proves type soundness via an operational semantics and an analysis of typing rules.