Hritcu, Catalin and Schwinghammer, Jan - A Step-indexed Semantics of Imperative Objects

lmcs:744 - Logical Methods in Computer Science, December 18, 2009, Volume 5, Issue 4
A Step-indexed Semantics of Imperative Objects

Authors: Hritcu, Catalin and Schwinghammer, Jan

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. 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, using step-indexing, one can interpret a rich type discipline with object types, subtyping, recursive and bounded quantified types in the presence of state.


Source : oai:arXiv.org:0906.1350
DOI : 10.2168/LMCS-5(4:2)2009
Volume: Volume 5, Issue 4
Published on: December 18, 2009
Submitted on: March 3, 2008
Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science,D.3.1,F.3.2


Share

Consultation statistics

This page has been seen 51 times.
This article's PDF has been downloaded 20 times.