Verified Spilling and Translation Validation with Repair
(pdf)
Julian Rosemann, Sigurd Schneider, Sebastian Hack
ITP
An Inductive Proof Method for Simulation-based Compiler Correctness
Sigurd Schneider, Gert Smolka, Sebastian Hack
Technical Report
A Linear First-Order Functional Intermediate Language for Verified Compilers
(pdf)
Sigurd Schneider, Gert Smolka, Sebastian Hack
Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015