L. R. Nielsen, “A Simple Correctness Proof of the Direct-Style Transformation”, BRICS, vol. 9, no. 2, Jan. 2002.