A unifying type-theoretic framework for objects

Abstract
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; Cooket al., 1990; Mitchell, 1990a) and encodings based on existential types (Pierce & Turner, 1994).

This publication has 20 references indexed in Scilit: