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.
http://i.stanford.edu/pub/cstr/reports/cs/tr/98/1602/CS-TR-98-1602.pdf