A Unifying Type-Theoretic Framework for Objects

We give a direct type-theoretic characterization of the basic mechanisms of object-oriented programming, including objects, methods, message passing, and subtyping, by introducing an explicit constructor for object types and suitable introduction, elimination, and equality rules. The resulting abstract framework provides a basis for justifying and comparing previous encodings of objects based on recursive record types (Cardelli, 1984; Cardelli, 1992; Bruce, 1994; Cook et al., 1990; Mitchell, 1990a) and encodings based on existential types (Pierce & Turner, 1994). 1 Introduction Research on the foundations of object-oriented programming languages has produced a series of increasingly ambitious attempts to capture the static typing properties of well-behaved programs in conventional object-oriented languages (Cardelli, 1984; Wand, 1987; Cook et al., 1990; Mitchell, 1990a; Cardelli, 1992; Bruce, 1994; Castagna et al., 1994; Pierce & Turner, 1994; Abadi, 1994; Abadi & Cardelli, 1994a; Aba..