Verified Inlining and Specialisation for PureCake

Abstract

Abstract Inlining is a crucial optimisation when compiling functional programming languages. This paper describes how we have implemented and verified function inlining and loop specialisation for PureCake, a verified compiler for a Haskell-like (purely functional, lazy) programming language. A novel aspect of our formalisation is that we justify inlining by pushing and pulling "Image missing"-bindings. All of our work has been mechanised in the HOL4 interactive theorem prover.