Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL. - Jan Olaf Blech; Sabine Glesner; Johannes Leitner; Steffen Mülling (COCV@ETAPS, 2005)