Machine Instruction Syntax and Semantics in Higher Order Logic. - Neophytos G. Michael; Andrew W. Appel (CADE, 2000)

A Trustworthy Proof Checker. - Andrew W. Appel; Neophytos G. Michael; Aaron Stump; Roberto Virga (J. Autom. Reason., 2003)