for a Type-Theoretic Model of Objects

We present a renement of the existential object model of Pierce and Turner [PT94]. In addition to signatures (or interfaces) as the types of objects, we also provide classes as the types of objects. These class types not only specify an interface, but also a particular implementation. We show that class types can be interpreted in the stan-dard PER model. Our main result is that the standard interpretation of subtyping in PER models { i.e. subtypes are subpers { is then behavioural subtyping in the sense of Leavens [Lea90].