Michael J. Butler, Thomas Långbacka: Program Derivation Using the Refinement Calculator. TPHOLs 1996: 93-108