Simple Type-Theoretic Foundations for Object-Oriented Programming

Abstract

Abstract We develop a formal, type-theoretic account of the basic mechanisms of object-oriented programming: encapsulation, message passing, subtyping and inheritance. By modelling object encapsulation in terms of existential types instead of the recursive records used in other recent studies, we obtain a substantial simplification both in the model of objects and in the underlying typed λ-calculus.