Bisimulations for untyped imperative objects

20Citations
Citations of this article
4Readers
Mendeley users who have this article in their library.

This artice is free to access.

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 [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.

Cite

CITATION STYLE

APA

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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free