L. R. Nielsen, “A Simple Correctness Proof of the Direct-Style Transformation”, BRICS, bd. 9, nr. 2, jan. 2002.