Z. Yang, “Reasoning About Code-Generation in Two-Level Languages”, BRICS, bd. 7, nr. 46, jun. 2000.