Xavier Leroy: Mechanized Semantics for Compiler Verification. CPP 2012: 4-6