Step-indexed semantic interpretations of types were proposed as an
alternative to purely syntactic proofs of type safety using subject reduction.
The types are interpreted as sets of values indexed by the number of
computation steps for which these values are guaranteed to behave like proper
elements of the type. Building on work by Ahmed, Appel and others, we introduce
a step-indexed semantics for the imperative object calculus of Abadi and
Cardelli.