J. Palsberg, “A Provably Correct Compiler Generator”, DPB, vol. 21, no. 382, Jan. 1992.