Publication details

Saarland University Computer Science

A Step-indexed Semantics of Imperative Objects (Extended Version)

Catalin Hritcu, Jan Schwinghammer

Technical Report, Programming Systems Lab, Saarland University, 2007

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.

Download PDF        Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009