We present a type inference algoritm and its
verification for an object-oriented programming
language called O'SMALL. O'SMALL is a class-based
language with imperative features. Classes are not
first-class citizens. No type declarations are
required.
Type inference operates on an extended lambda-calculus
into which O'SMALL is translated. The system features
extensible record types, mu-types, and imperative
types.
This work belongs to both theoretical and practical
computer science. In the theoretical part, the type
inference algoritm for our lambda-calculus with records
is formalized in order-sorted logic. In the practical
part, the algoritm for let-polymorphism and imperative
features is based on well-known approaches. These
approaches are presented in a new fashion but they are
not proven correct.
Doctoral Thesis, April 1994, Saarland University