Abstract
We develop a general method of proving contextual properties—including (but not limited to) observational equivalence, space improvement, and memory safety under arbitrary contexts—for programs in untyped call-by-value λ-calculus with first-class, higher-order references (ref, : = and !) and deallocation (free). The method significantly generalizes Sumii et al.’s environmental bisimulation technique, and gives a sound and complete characterization of each proved property, in the sense that the “bisimilarity” (the largest set satisfying the bisimulation-like conditions) equals the set of terms with the property to be proved. We give examples of contextual properties concerning typical data structures such as linked lists, binary search trees, and directed acyclic graphs with reference counts, all with deletion operations that release memory.
This shows the scalability of the environmental approach from contextual equivalence to other binary relations (such as space improvement) and unary predicates (such as memory safety), as well as to languages with non-monotone store, where Kripke-style logical relations have difficulties.
Extended abstract with appendices online [13].
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ahmed, A.: Semantics of Types for Mutable State. PhD thesis, Princeton University (2004)
Ahmed, A., Dreyer, D., Rossberg, A.: State-dependent representation independence. In: Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2009) (to appear), http://ttic.uchicago.edu/~amal/papers/sdri.pdf
Ahmed, A., Fluet, M., Morrisett, G.: A step-indexed model of substructural state. In: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming, pp. 78–91 (2005)
Ahmed, A., Fluet, M., Morrisett, G.: L3: A linear language with locations. TLCA 2005 77(4), 397–449 (2007); extended abstract appeared in: Typed Lambda Calculi and Applications. LNCS, vol. 3461, pp. 293–307. Springer (2005)
Bohr, N.: Advances in Reasoning Principles for Contextual Equivalence and Termination. PhD thesis, IT University of Copenhagen (2007)
Crary, K., Walker, D., Morrisett, G.: Typed memory management in a calculus of capabilities. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 262–275 (1999)
Koutavas, V., Wand, M.: Small bisimulations for reasoning about higher-order imperative programs. In: Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 141–152 (2006)
Meyer, A.R., Sieber, K.: Towards fully abstract semantics for local variables: Preliminary report. In: Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 191–203 (1988)
Mitchell, J.C.: Foundations for Programming Languages. MIT Press, Cambridge (1996)
Morris Jr., J.H.: Lambda-Calculus Models of Programming Languages. PhD thesis, Massachusetts Institute of Technology (1968)
Pitts, A.M., Stark, I.: Operational reasoning for functions with local state. In: Higher Order Operational Techniques in Semantics, pp. 227–273. Cambridge University Press, Cambridge (1998)
Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order languages. In: Twenty-Second Annual IEEE Symposium on Logic in Computer Science, pp. 293–302 (2007)
Sumii, E.: A theory of non-monotone memory (or: Contexts for free), http://www.kb.ecei.tohoku.ac.jp/~sumii/pub/non-mono.pdf
Sumii, E., Pierce, B.C.: A bisimulation for dynamic sealing. Theoretical Computer Science 375, 1–3, 169–192 (2007); extended abstract appeared in: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 161–172 (2004)
Sumii, E., Pierce, B.C.: A bisimulation for type abstraction and recursion. Journal of the ACM 54, 5–26, 1–43 (2007); extended abstract appeared in: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 63–74 (2005)
Tofte, M., Talpin, J.-P.: Implementation of the typed call-by-value λ-calculus using a stack of regions. In: Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 188–201 (1994)
Wadler, P.: Linear types can change the world! In: Programming Concepts and Methods. North Holland, Amsterdam (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sumii, E. (2009). A Theory of Non-monotone Memory (Or: Contexts for free). In: Castagna, G. (eds) Programming Languages and Systems. ESOP 2009. Lecture Notes in Computer Science, vol 5502. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00590-9_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-00590-9_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00589-3
Online ISBN: 978-3-642-00590-9
eBook Packages: Computer ScienceComputer Science (R0)