J. Palsberg, “An Automatically Generated and Provably Correct Compiler for a Subset of Ada”, DPB, vol. 21, no. 383, Jan. 1992.