Nielsen, L. R. “A Simple Correctness Proof of the Direct-Style Transformation”. BRICS Report Series, vol. 9, no. 2, Jan. 2002, doi:10.7146/brics.v9i2.21719.