Z. Yang, “Reasoning About Code-Generation in Two-Level Languages”, BRICS, vol. 7, no. 46, Jun. 2000.