Compilation as Rewriting in Higher Order Logic
CADE, pp. 19-34, 2007.
mechanical applicationentire compilerprogram transformationhigher order logiclogical frameworkMore(3+)
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
Full Text (Upload PDF)
PPT (Upload PPT)