A bisimulation-like proof method for contextual properties in untyped λ-calculus with references and deallocation

研究成果: Article

2 引用 (Scopus)

抜粋

We develop a general method for proving properties of programs under arbitrary contextsincluding (but not limited to) observational equivalence, space improvement, and a form of memory safety of the programsin untyped call-by-value λ-calculus with first-class, dynamically allocated, higher-order references and deallocation. The method 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.

元の言語English
ページ(範囲)4358-4378
ページ数21
ジャーナルTheoretical Computer Science
411
発行部数51-52
DOI
出版物ステータスPublished - 2010 12 4

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

フィンガープリント A bisimulation-like proof method for contextual properties in untyped λ-calculus with references and deallocation' の研究トピックを掘り下げます。これらはともに一意のフィンガープリントを構成します。

  • これを引用