We give semantics to Moby by formalizing the surface language in an external language (EL) and then translating the external language to an internal language (IL) in the style of Harper and Stone. We designed our EL, called MicroMoby, to study the class construct in Moby. Our IL, called MOC, is a new extensible-object calculus designed to provide semantic foundations to our class construct. MOC includes both a static and dynamic semantics, and we prove a subject reduction theorem for the calculus. We give a translation from MicroMoby programs into MOC terms and prove that this translation preserves types. A consequence of this theorem and type-safety for MOC is that MicroMoby is type-safe. The semantics presented here provides a precise characterization of the interaction between Moby's object and class mechanisms.
This work is joint with John Reppy of Bell Labs.