Palsberg, J. A Provably Correct Compiler Generator. DPB 1992, 21.