This artice is free to access.
We present a sound and complete method for reasoning about contextual equivalence in the untyped, imperative object calculus of Abadi and Cardelli . Our method is based on bisimulations, following the work of Sumii and Pierce [25, 26] and our own . Using our method we were able to prove equivalence in more complex examples than the ones of Gordon, Hankin and Lassen  and Gordon and Rees . We can also write bisimulations in closed form in cases where similar bisimulation methods  require an inductive specification. To derive our bisimulations we follow the same technique as we did in , thus indicating the extensibility of this method. © Springer-Verlag Berlin Heidelberg 2006.
Koutavas, V., & Wand, M. (2006). Bisimulations for untyped imperative objects. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3924 LNCS, pp. 146–161). https://doi.org/10.1007/11693024_11