Computer Science – Programming Languages
Scientific paper
2009-06-07
LMCS 5 (4:2) 2009
Computer Science
Programming Languages
Scientific paper
10.2168/LMCS-5(4:2)2009
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.
Hritcu Catalin
Schwinghammer Jan
No associations
LandOfFree
A Step-indexed Semantics of Imperative Objects does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with A Step-indexed Semantics of Imperative Objects, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A Step-indexed Semantics of Imperative Objects will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-370131