Compilation as Rewriting in Higher Order Logic

CADE, pp. 19-34, 2007.

Cited by: 16|Bibtex|Views0|Links
EI
Keywords:
mechanical applicationentire compilerprogram transformationhigher order logiclogical frameworkMore(3+)

Abstract:

We present an approach based on the use of deductive rewriting to construct a trusted compiler for a subset of the native functions of higher order logic. Program transformations are specified by equality theorems that characterize the transformations; and the mechanical application of these rules is directed by programs written in the me...More

Code:

Data:

Your rating :
0

 

Tags
Comments