Mosses, P. D. A Constructive Approach to Compiler Correctness. DPB 1980, 9.