  We describe an approach to the verified implementation of transformations on
functional programs that exploits the higher-order representation of syntax. In
this approach, transformations are specified using the logic of hereditary
Harrop formulas. On the one hand, these specifications serve directly as
implementations, being programs in the language Lambda Prolog. On the other
hand, they can be used as input to the Abella system which allows us to prove
properties about them and thereby about the implementations. We argue that this
approach is especially effective in realizing transformations that analyze
binding structure. We do this by describing concise encodings in Lambda Prolog
for transformations like typed closure conversion and code hoisting that are
sensitive to such structure and by showing how to prove their correctness using
Abella.
