Bisimilarity for a first-order calculus of objects with subtyping

AD Gordon, GD Rees - Proceedings of the 23rd ACM SIGPLAN-SIGACT …, 1996 - dl.acm.org
AD Gordon, GD Rees
Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of …, 1996dl.acm.org
Bisimilarity (also known as' applicative bisimulation') has attracted a good deal of attention
as an operational equivalence for λ-calculi. It approximates or even equals Morris-style
contextual equivalence and admits proofs of program equivalence via co-induction. It has an
elementary construction from the operational definition of a language. We consider
bisimilarity for one of the typed object calculi of Abadi and Cardelli. By defining a labelled
transition system for the calculus in the style of Crole and Gordon and using a variation of …
Bisimilarity (also known as 'applicative bisimulation') has attracted a good deal of attention as an operational equivalence for λ-calculi. It approximates or even equals Morris-style contextual equivalence and admits proofs of program equivalence via co-induction. It has an elementary construction from the operational definition of a language. We consider bisimilarity for one of the typed object calculi of Abadi and Cardelli. By defining a labelled transition system for the calculus in the style of Crole and Gordon and using a variation of Howe's method we establish two central results: that bisimilarity is a congruence, and that it equals contextual equivalence. So two objects are bisimilarity no amount of programming can tell them apart. Our third contribution is to show that bisimilarity soundly models the equational theory of Abadi and Cardelli. This is the first study of contextual equivalence for an object calculus and the first application of Howe's method to subtyping. By these results, we intend to demonstrate that operational methods are a promising new direction for the foundations of object-oriented programming.
ACM Digital Library