T. P. Lange, “The Correctness of an Optimized Code Generation”, DPB, vol. 21, no. 427, Nov. 1992.