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. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
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
Mendeley helps you to discover research relevant for your work.