Data refinement, call by value and higher order programs
David A. Naumann · Formal Aspects of Computing · 1995
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.