Extensible Proof-Producing Compilation
Compiler Construction, pp. 2-16, 2009.
small lisp-like languagemachine codehol4 theorem proverproof-producing compilationsource functionMore(6+)
This paper presents a compiler which produces machine code from functions dened in the logic of a theorem prover, and at the same time proves that the generated code executes the source functions. Un- like previously published work on proof-producing compilation from a theorem prover, our compiler provides broad support for user-dened ext...More
PPT (Upload PPT)