Publication details

Saarland University Computer Science

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

Catalin Hritcu, Jan Schwinghammer

Workshop Proceedings Foundations of Object-Oriented Languages (FOOL'08), pp. 1--13, 2008

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.

Superseded by LMCS journal version.

Full proofs can be found in this technical report

Download PDF        Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009