A Proof-Producing Software Compiler for a Subset of Higher Order Logic

We discuss a proof-producing compiler which translates first order recursion equations, defined in higher order logic, to assembly lan- guage. The front end of the compiler is based on a series of source-to- source translations, starting with a semantic CPS translation and cul- minating in graph-colouring register allocation. Equality of the original program and the result of register allocation is proved automatically. A translation validation assertion is then generated, relating values of the original function to the result of running the compiled code on a subset of the ARM machine. Approaches to the automatic proof of this formula are also discussed.