Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic

We give an overview of a proof-producing compiler which translates recursion equations, defined in higher order logic, to assembly language. The compiler is implemented and validated with a mix of translation validation and compiler verification techniques. Both the design of the compiler and its mechanical verification are implemented in the same logic framework.

• Type: Conference
• Year: 2007
• Where: ESOP
• Authors: Guodong Li, Scott Owens, Konrad Slind
• Keywords: Compiler, Compiler Verification Techniques, ESOP 2007, Programming Languages, Proof-producing Compiler