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