Extensible Proof-Producing Compilation

Compiler Construction, pp. 2-16, 2009.

Cited by: 21|Bibtex|Views5|Links
EI
Keywords:
small lisp-like languagemachine codehol4 theorem proverproof-producing compilationsource functionMore(6+)

Abstract:

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

Code:

Data:

Your rating :
0

 

Tags
Comments