O. Danvy and K. Millikin, “A Simple Application of Lightweight Fusion to Proving the Equivalence of Abstract Machines”, BRICS, vol. 14, no. 8, Mar. 2007.