Data refinement, call by value and higher order programs

Abstract

Using 2-categorical laws of algorithmic refinement, we show soundness of data refinement for stored programs and hence for higher order procedures with value/result parameters. The refinement laws hold in a model that slightly generalizes the standard predicate transformer semantics for the usual imperative programming constructs including prescriptions.