Abstract
We present a refinement of the existential object model of Pierce
and Turner. 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 standard PER model.
Our main result is that the standard interpretation of subtyping in
PER models - i.e. subtypes are subpers - is then exactly the
notion of behavioural subtyping as it is defined by Leavens.