A Formal Correctness Proof for Code Generation from SSA Form in Isabelle/HOL.

Jan Olaf Blech, Sabine Glesner

Browse the full GI paper archive.