Palsberg, J. Provably Correct Compiler Generation. DPB 1992, 21.