A theory of non-monotone memory (or: Contexts for free)

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

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

Original languageEnglish
Title of host publicationProgramming Languages and Systems - 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, Proceedings
Pages237-251
Number of pages15
DOIs
Publication statusPublished - 2009 Jul 15
Event18th European Symposium on Programming, ESOP 2009 - York, United Kingdom
Duration: 2009 Mar 222009 Mar 29

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5502
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other18th European Symposium on Programming, ESOP 2009
CountryUnited Kingdom
CityYork
Period09/3/2209/3/29

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A theory of non-monotone memory (or: Contexts for free)'. Together they form a unique fingerprint.

  • Cite this

    Sumii, E. (2009). A theory of non-monotone memory (or: Contexts for free). In Programming Languages and Systems - 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, Proceedings (pp. 237-251). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5502). https://doi.org/10.1007/978-3-642-00590-9_18