Compilation as rewriting in higher order logic

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 metalanguage of the logical framework. Each application of a rule ensures that the transformed code is equivalent to the original one, thus warranting the correctness of the entire compiler. © Springer-Verlag Berlin Heidelberg 2007.