Bisimulations for Untyped Imperative Objects

We present a sound and complete method for reasoning about contextual equivalence in the untyped, imperative object calculus of Abadi and Cardelli [1]. Our method is based on bisimulations, following the work of Sumii and Pierce [25, 26] and our own [14]. Using our method we were able to prove equivalence in more complex examples than the ones of Gordon, Hankin and Lassen [7] and Gordon and Rees [8]. We can also write bisimulations in closed form in cases where similar bisimulation methods [26] require an inductive specification. To derive our bisimulations we follow the same technique as we did in [14], thus indicating the extensibility of this method.

• Type: Conference
• Year: 2006
• Where: ESOP
• Authors: Vasileios Koutavas, Mitchell Wand
• Keywords: Complete Method, Contextual Equivalence, ESOP 2006, Imperative Object Calculus, Programming Languages