Jan Olaf Blech, Sabine Glesner, Johannes Leitner, Steffen Mülling
Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL
COCV, 2005.
@article{COCV-J-2005-BlechGLM, author = "Jan Olaf Blech and Sabine Glesner and Johannes Leitner and Steffen Mülling", doi = "10.1016/j.entcs.2005.02.042", journal = "{Electronic Notes in Theoretical Computer Science}", number = 2, pages = "33--51", title = "{Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL}", volume = 141, year = 2005, }