Soundness of data refinement for a higher-order imperative language

Using a set-theoretic model of predicate transformers and ordered data types, we give a semantics for an Oberon-like higher-order imperative language with record subtyping and procedure-type variables and parameters. Data refinement is shown to be sound for this language: It implies algorithmic refinement when suitably localized. All constructs are shown to preserve simulation, so data refinement can be carried out piecewise.