Step-indexed semantic models of types were proposed as an alternative to purely syntactic proofs of type safety using subject reduction. Building on work by Ahmed, Appel and others, we introduce a step-indexed model for the imperative object calculus of Abadi and Cardelli. Providing a semantic account of this calculus using more 'traditional', domain-theoretic approaches has proved challenging due to the combination of dynamically allocated objects, higher-order store, and an expressive type system. Here we show that the step-indexed model can interpret a rich type discipline with object types, subtyping, recursive and bounded quantified types in the presence of state.
Presented at FOOL'08; Sunday, 13 January 2007; San Francisco, California, USA.