Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Bisimulations for Untyped Imperative Objects

Vasileios KoutavasContact Information and Mitchell WandContact Information

(1)  Northeastern University,  
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.

Contact Information Vasileios Koutavas
Email: vkoutav@ccs.neu.edu

Contact Information Mitchell Wand
Email: wand@ccs.neu.edu
Fulltext Preview (Small, Large)
Image of the first page of the fulltext


Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.110 • Server: mpweb22
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)