Jan Olaf Blech, Sabine Glesner: A Formal Correctness Proof for Code Generation from SSA Form in Isabelle/HOL. GI Jahrestagung (2) 2004: 449-458