Case Studies in Compiler Correctness Using HOL. - David F. Martin; R. J. Toal (TPHOLs, 1991)