Typed Interpretations of Extensible Objects

This paper describes a type preserving and computationally adequate interpretation of a full-edged object calculus that supports message passing and constructs for object update and extension. The target theory is a higher-order -calculus with records and recursive folds/unfolds, polymorphic and recursive types, and subtyping. The interpretation specializes to calculi of nonextensible objects, and validates the expected subtyping relationship