@InProceedings{KoutavasWand06esop,
  author    = {Vasileios Koutavas and Mitchell Wand},
  title     = {Bisimulations for Untyped Imperative Objects},
  editor    = {Peter Sestoft},
  booktitle = {Programming Languages and Systems, 15th European
               Symposium on Programming, ESOP 2005, Vienna, Austria.},
  publisher = {Springer-Verlag},
  series    = {Lecture Notes in Computer Science},
  volume    = {3924},
  year      = {2006},
  pages     = {146-161},
  abstract  = {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 [26, 27] and our own [15]. 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 [27] require an inductive specification. To derive
our bisimulations we follow the same technique as we did in [15], thus
indicating the extensibility of this method.},

}