A bisimulation-like proof method for contextual properties in untyped \(\lambda \)-calculus with references and deallocation

DOI10.1016/j.tcs.2010.09.009zbMath1235.68112OpenAlexW2085589490MaRDI QIDQ615949

Eijiro Sumii

Publication date: 7 January 2011

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2010.09.009

zbMATH Keywords

contextual equivalenceenvironmental bisimulationlocal memory safetymemory management and deallocation

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• A step-indexed model of substructural state
• A bisimulation for type abstraction and recursion
• A Complete Characterization of Observational Equivalence in Polymorphic λ-Calculus with General References
• State-dependent representation independence
• Small bisimulations for reasoning about higher-order imperative programs
• A bisimulation for dynamic sealing
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A bisimulation-like proof method for contextual properties in untyped \(\lambda \)-calculus with references and deallocation