Optimizing Stack Allocation for the CakeML Compiler

Abstract

This thesis concerns the formal verification of an optimization in relation to memory stack allocation and deallocation operations in the context of tail calls, in an intermediate language of the CakeML compiler. The thesis explores and provides a discourse on the implementation and associated proof of a compiler phase in a verified compiler in which the semantics of each phase must be correct with respect to the previous one. CakeML is a functional programming language based on Standard ML, and has a compiler that is fully verified. A primary focus in this thesis is put on the formal proof, where the optimization and its implementation merely serve as a foundation.