Much of the work on developing type-theoretic foundations for object-oriented programming languages has its roots in the typed lambda calculus. In such approaches, an object is viewed as a record of functions together with a hidden representation type.
...the fact that objects in real object-oriented languages change state is either ignored or dealt with in an indirect way.
...in [concurrent object-oriented] languages, "active objects" may have their own thread of control and may delay the servicing of certain requests according to synchronization constraints.
Existing notions of types [...] do not address the issues of non-uniform availability or conformance to a service protocol.
It is essential to start viewing an object as a process, not as function.
[...] what we believe types are [...]. We are interested in viewing types as partial specifications of behaviour [...]. Naturally we would also like these specifications to [...] be statically checkable.
If we think of objects as "servers", then the services they provide are promises that they understand certain types of requests, and that [...] they will eventually send [...] certain types of reply.
If requests must be sent in a certain order or if certain services may be temporarily unavailable, the object's type should describe this. Type safety, in this case means that clients [will] not deadlock because of protocol errors. Type substitutability is correspondingly defined so that sequences of interactions that are valid for a supertype are also valid for a subtype.
[...] it is correct to view the object's protocol as inherently non-deterministic, since it would be unreasonable to expect clients to monitor the environment to know the state of an object's protocol.