Report Number: CS-TR-98-1602
Institution: Stanford University, Department of Computer Science
Title: Type Systems for Object-Oriented Programming Languages
Author: Fisher, Kathleen
Date: February 1998
Abstract: Object-oriented programming languages (OOPL's) provide important support for today's large-scale software projects. Unfortunately, typed OOPL's have suffered from overly restrictive type systems that have forced programmers to use type-casts to achieve flexibility, a notorious source of hard-to-find bugs. One source of this inflexibility is the conflation of subtyping and inheritance, which reduces potential code reuse. Attempts to fix this rigidity have resulted in unsound type systems, most notably Eiffel's. This thesis develops a sound type system for a formal object-oriented language. It gains flexibility by separating subtyping and inheritance and by supporting method specialization, which allows the types of methods to be refined during inheritance. The lack of such a mechanism is a key source of type-casts in languages like C++. Abstraction primitives in this formal language support a class construct similar to the one found in C++ and Java, explaining the link between inheritance and subtyping: object types that include implementation information are a form of abstract type, and the only way to produce a subtype of an abstract type is via inheritance. Formally, the language is presented as an object calculus. The thesis proves type soundness with respect to an operational semantics via a subject reduction theorem.