It has been widely recognized that while object orientation brings tangible practical benefits to the software development process, its theoretical underpinnings are less clear. This paper fits within a body of research that is responding to this problem. It does this by presenting an encoding of Abadi and Cardelli’s object calculus (OC) into the &pgr;-calculus.

One possible criticism of this activity is that it takes a rather esoteric and theoretical calculus, OC, and encodes it into another esoteric and theoretical calculus, the &pgr;-calculus. However, a contrary position is that the encoding links practical imperative programming languages to the &pgr;-calculus, since encodings of such languages into OC already exist. Furthermore, the work gives further evidence that the &pgr;-calculus is a foundational model for object orientation, in the sense that a wide spectrum of object-oriented notations can be encoded in it.

A particular contribution of this paper is that it emphasizes typing in such encoding exercises and presents impressive theoretical results on this topic. These results ensure that under the translation, the types in OC agree (in some well-defined sense) with the types in the &pgr;-calculus.

In order to obtain this agreement, a particular dialect of the &pgr;-calculus is proposed that uses variant types and a case construct rather than tupling and matching. Using this dialect, subtle problems surrounding the self parameter in OC methods are resolved at the expense of a relatively complex encoding. One important question that the paper leaves unanswered is how the proposed &pgr;-calculus dialect relates to other &pgr;-calculus incarnations. This is, of course, an important issue if a single foundational theory is being sought.