A kripke logical relation for effect-based program transformations
Jacob Thamsborg, Lars Birkedal · 2011
We present a Kripke logical relation for showing the correctness of program transformations based on a type-and-effect system for an ML-like programming language with higher-order store and dynamic allocation.