Sciweavers

CC
2009
Springer

Extensible Proof-Producing Compilation

14 years 4 months ago
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.
Magnus O. Myreen, Konrad Slind, Michael J. C. Gord
Added 22 Nov 2009
Updated 22 Nov 2009
Type Conference
Year 2009
Where CC
Authors Magnus O. Myreen, Konrad Slind, Michael J. C. Gordon
Comments (0)