Yang, Z. Reasoning About Code-Generation in Two-Level Languages. BRICS 2000, 7.