Moby is a statically typed, ML-like language that supports class-based object-oriented programming. Our design philosophy is to keep language features independent, but complementary. Moby's support for class-based object-oriented programming is a prime example of this philosophy: classes provide support for object creation and inheritance, but we rely on the module system for information hiding and on object types for subtyping. The resulting design is both simple and expressive.
In this paper, we give semantics to the object-oriented features of Moby in the style of Harper and Stone. We formalize the surface language in an external language, called MicroMoby, and define a type-preserving translation from MicroMoby to an internal language, called MOC. We designed MicroMoby to study the class and object constructs in Moby. The internal language MOC is a new extensible-object calculus designed to provide semantic foundations for MicroMoby. We present both the static and dynamic semantics of MOC, and prove a subject reduction theorem. We also present the translation from MicroMoby to MOC and prove that this translation preserves types. A consequence of this theorem and type-safety for MOC is that MicroMoby is type-safe.