A kripke logical relation for effect-based program transformations

Abstract

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.