J. Palsberg, “Provably Correct Compiler Generation”, DPB, vol. 21, no. 422, Oct. 1992.