Types and Invariants in the Refinement Calculus. - Carroll Morgan; Trevor Vickers (Sci. Comput. Program., 1990)