Palsberg, J. An Automatically Generated and Provably Correct Compiler for a Subset of Ada. DPB 1992, 21.