Extensible Proof-Producing Compilation

This paper presents a compiler which produces machine code from functions defined in the logic of a theorem prover, and at the same time proves that the generated code executes the source functions. Unlike previously published work on proof-producing compilation from a theorem prover, our compiler provides broad support for user-defined extensions, targets multiple carefully modelled commercial machine languages, and does not require termination proofs for input functions. As a case study, the compiler is used to construct verified interpreters for a small LISP-like language. The compiler has been implemented in the HOL4 theorem prover.

• Type: Conference
• Year: 2009
• Where: CC
• Authors: Magnus O. Myreen, Konrad Slind, Michael J. C. Gordon
• Keywords: CC 2009, Input Functions, Modelled Commercial Machine, Programming Languages, Theorem Prover