Optimizing Stack Allocation for the CakeML Compiler
Examensarbete för masterexamen
Computer science – algorithms, languages and logic (MPALG), MSc
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.
Verification , Formal Methods , Compiler Optimizations, , Functional Programming , CakeML