Abstract
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. © 2009 Springer Berlin Heidelberg.
Cite
CITATION STYLE
Myreen, M. O., Slind, K., & Gordon, M. J. C. (2009). Extensible proof-producing compilation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5501 LNCS, pp. 2–16). https://doi.org/10.1007/978-3-642-00722-4_2
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
