More Web Proxy on the site http://driver.im/

Article

Bisimulations for untyped imperative objects

Authors:

Vasileios Koutavas,

Mitchell WandAuthors Info & Claims

ESOP'06: Proceedings of the 15th European conference on Programming Languages and Systems

Pages 146 - 161

https://doi.org/10.1007/11693024_11

Published: 27 March 2006 Publication History

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.

References

[1]

Martín Abadi and Luca Cardelli. A Theory of Objects. Springer-Verlag, Berlin, Heidelberg, and New York, 1996.

Digital Library

[2]

Samson Abramsky. The lazy lambda calculus. In David A. Turner, editor, Research Topics in Functional Programming, pages 65-116. Addison-Wesley, 1990.

Digital Library

[3]

Nick Benton and Benjamin Leperchey. Relational reasoning in a nominal semantics for storage. In Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings, volume 3461 of Lecture Notes in Computer Science, pages 86-101. Springer, 2005.

Digital Library

[4]

Gavin Bierman, Matthew Parkinson, and Andrew Pitts. MJ: An imperative core calculus for Java and Java with effects. Technical Report 563, Cambridge University Computer Laboratory, April 2003.

[5]

Yuxin Deng and Davide Sangiorgi. Towards an algebraic theory of typed mobile processes. In ICALP, volume 3142 of Lecture Notes in Computer Science, pages 445-456. Springer-Verlag, 2004.

[6]

Matthew Flatt, Shriram Krishnamurthi, and Matthias Felleisen. A programmer's reduction semantics for classes and mixins. In Formal Syntax and Semantics of Java, pages 241-269, London, UK, 1999. Springer-Verlag.

Digital Library

[7]

Andrew D. Gordon, Paul D. Hankin, and Soren B. Lassen. Compilation and equivalence of imperative objects. In Proceedings of the 17th Conference on Foundations of Software Technology and Theoretical Computer Science, pages 74-87, London, UK, 1997. Springer-Verlag.

Digital Library

[8]

Andrew D. Gordon and Gareth D. Rees. Bisimilarity for a first-order calculus of objects with subtyping. In Proceedings 23rd Annual ACM Symposium on Principles of Programming Languages, pages 386-395, New York, NY, USA, 1996. ACM Press.

Digital Library

[9]

Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In ICALP, pages 299-309, 1980.

Digital Library

[10]

Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32:137-161, 1985.

Digital Library

[11]

Douglas J. Howe. Equality in lazy computation systems. In Proc. 4th IEEE Symposium on Logic in Computer Science, pages 198-203, 1989.

Digital Library

[12]

Cliff B. Jones. A pi-calculus semantics for an object-based design notation. In Eike Best, editor, CONCUR, volume 715 of Lecture Notes in Computer Science, pages 158-172. Springer, 1993.

Digital Library

[13]

Josva Kleist and Davide Sangiorgi. Imperative objects as mobile processes. Sci. Comput. Program., 44(3):293-342, 2002.

Digital Library

[14]

Vasileios Koutavas and Mitchell Wand. Smaller bisimulations for reasoning about higher-order imperative programs. In Proceedings 33rd Annual ACM Symposium on Principles of Programming Languages, New York, NY, USA, 2006. ACM Press.

Digital Library

[15]

Xinxin Liu and David Walker. Partial confluence of processes and systems of objects. Theor. Comput. Sci., 206(1-2):127-162, 1998.

Digital Library

[16]

Ian A. Mason and Carolyn L. Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1:287-327, 1991.

[17]

Albert R. Meyer and Kurt Sieber. Towards fully abstract semantics for local variables: Preliminary report. In Proceedings 15th Annual ACM Symposium on Principles of Programming Languages, pages 191-203, 1988.

Digital Library

[18]

Robert Milne and Christopher Strachey. A Theory of Programming Language Semantics. Chapman and Hall, London, 1976. Also Wiley, New York.

Digital Library

[19]

James H. Morris, Jr. Lambda Calculus Models of Programming Languages. PhD thesis, MIT, Cambridge, MA, 1968.

[20]

Andrew Pitts and Ian Stark. Operational reasoning for functions with local state. In Andrew Gordon and Andrew Pitts, editors, Higher Order Operational Techniques in Semantics, pages 227-273. Publications of the Newton Institute, Cambridge University Press, 1998.

Digital Library

[21]

D. Sangiorgi. Locality and non-interleaving semantics in calculi for mobile processes. Theoretical Computer Science, 155:39-83, 1996.

Digital Library

[22]

D. Sangiorgi. On the bisimulation proof method. Mathematical. Structures in Comp. Sci., 8(5):447-479, 1998.

Digital Library

[23]

D. Sangiorgi and R. Milner. The problem of "Weak Bisimulation up to". In W.R. Cleveland, editor, Proc. CONCUR '92, volume 630 of Lecture Notes in Computer Science, pages 32-46. Springer-Verlag, 1992.

Digital Library

[24]

Davide Sangiorgi. An interpretation of typed objects into typed π-calculus. Inf. Comput., 143(1):34-73, 1998.

Digital Library

[25]

Eijiro Sumii and Benjamin C. Pierce. A bisimulation for dynamic sealing. In Proceedings 31st Annual ACM Symposium on Principles of Programming Languages, pages 161-172, New York, NY, USA, 2004. ACM Press.

Digital Library

[26]

Eijiro Sumii and Benjamin C. Pierce. A bisimulation for type abstraction and recursion. In Proceedings 32nd Annual ACM Symposium on Principles of Programming Languages, pages 63-74, New York, NY, USA, 2005. ACM Press.

Digital Library

[27]

David Walker. Objects in the π-calculus. Inf. Comput., 116(2):253-271, 1995.

Digital Library

Cited By

Samak MKim DRinard M(2019)Synthesizing replacement classesProceedings of the ACM on Programming Languages10.1145/33711204:POPL(1-33)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371120
Sangiorgi DVignudelli V(2019)Environmental Bisimulations for Probabilistic Higher-order LanguagesACM Transactions on Programming Languages and Systems10.1145/335061841:4(1-64)Online publication date: 12-Oct-2019
https://dl.acm.org/doi/10.1145/3350618
Wang YDillig ILahiri SCook W(2017)Verifying equivalence of database-driven applicationsProceedings of the ACM on Programming Languages10.1145/31581442:POPL(1-29)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158144
Show More Cited By

Recommendations

Small bisimulations for reasoning about higher-order imperative programs
Proceedings of the 2006 POPL Conference

We introduce a new notion of bisimulation for showing contextual equivalence of expressions in an untyped lambda-calculus with an explicit store, and in which all expressed values, including higher-order values, are storable. Our notion of bisimulation ...
Small bisimulations for reasoning about higher-order imperative programs
POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We introduce a new notion of bisimulation for showing contextual equivalence of expressions in an untyped lambda-calculus with an explicit store, and in which all expressed values, including higher-order values, are storable. Our notion of bisimulation ...
Compilation and equivalence of imperative objects

We adopt the untyped imperative object calculus of Abadi and Cardelli as a minimal setting in which to study problems of compilation and program equivalence that arise when compiling object-oriented languages. We present both a big-step and a small-step ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ESOP'06: Proceedings of the 15th European conference on Programming Languages and Systems

March 2006

342 pages

ISBN:354033095X

Editor:
Peter Sestoft
IT University of Copenhagen, Denmark

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 27 March 2006

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Samak MKim DRinard M(2019)Synthesizing replacement classesProceedings of the ACM on Programming Languages10.1145/33711204:POPL(1-33)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371120
Sangiorgi DVignudelli V(2019)Environmental Bisimulations for Probabilistic Higher-order LanguagesACM Transactions on Programming Languages and Systems10.1145/335061841:4(1-64)Online publication date: 12-Oct-2019
https://dl.acm.org/doi/10.1145/3350618
Wang YDillig ILahiri SCook W(2017)Verifying equivalence of database-driven applicationsProceedings of the ACM on Programming Languages10.1145/31581442:POPL(1-29)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158144
Sangiorgi DVignudelli V(2016)Environmental bisimulations for probabilistic higher-order languagesACM SIGPLAN Notices10.1145/2914770.283765151:1(595-607)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2914770.2837651
Sangiorgi DVignudelli VBodik RMajumdar R(2016)Environmental bisimulations for probabilistic higher-order languagesProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2837614.2837651(595-607)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2837614.2837651
Welsch YPoetzsch-Heffter AChin WHobor A(2012)Verifying backwards compatibility of object-oriented libraries using BoogieProceedings of the 14th Workshop on Formal Techniques for Java-like Programs10.1145/2318202.2318209(35-41)Online publication date: 12-Jun-2012
https://dl.acm.org/doi/10.1145/2318202.2318209
Tzevelekos N(2012)Program equivalence in a simple language with stateComputer Languages, Systems and Structures10.1016/j.cl.2012.02.00238:2(181-198)Online publication date: 1-Jul-2012
https://dl.acm.org/doi/10.1016/j.cl.2012.02.002
Sangiorgi DKobayashi NSumii E(2011)Environmental bisimulations for higher-order languagesACM Transactions on Programming Languages and Systems10.1145/1889997.189000233:1(1-69)Online publication date: 25-Jan-2011
https://dl.acm.org/doi/10.1145/1889997.1890002
Welsch YPoetzsch-Heffter A(2011)Full abstraction at package boundaries of object-oriented languagesProceedings of the 14th Brazilian conference on Formal Methods: foundations and Applications10.1007/978-3-642-25032-3_3(28-43)Online publication date: 26-Sep-2011
https://dl.acm.org/doi/10.1007/978-3-642-25032-3_3
Silva LNaumann DSampaio A(2010)Refactoring and representation independence for class hierarchiesProceedings of the 12th Workshop on Formal Techniques for Java-Like Programs10.1145/1924520.1924528(1-7)Online publication date: 22-Jun-2010
https://dl.acm.org/doi/10.1145/1924520.1924528
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents