Palsberg, J. “An Automatically Generated and Provably Correct Compiler for a Subset of Ada”. DAIMI Report Series, vol. 21, no. 383, Jan. 1992, doi:10.7146/dpb.v21i383.6615.