Verified Function Inlining Optimization fro the PureCake Compiler

Abstract

This thesis describes the implementation and formal verification of an inlining optimization pass for the PureCake compiler. PureCake is a verified optimizing compiler for a pure, lazy, functional programming language. The optimization is implemented and verified using the HOL4 theorem prover. The correctness proof of inlining is defined at two levels of abstraction. The meta-theory level and the compiler level. The implementation is heuristic agnostic and can be used with any inlining strategy. The thesis also describes a function specialization transformation. This transformation is unverified, but steps are described on how the current inlining implementation and methodology can be used to verify it.