Nielsen, L. R. A Simple Correctness Proof of the Direct-Style Transformation. BRICS 2002, 9.