Optimizing Stack Allocation for the CakeML Compiler
Ladda ner
Typ
Examensarbete för masterexamen
Master's Thesis
Master's Thesis
Program
Computer science – algorithms, languages and logic (MPALG), MSc
Publicerad
2023
Författare
Ahlin, Richard
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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.
Beskrivning
Ämne/nyckelord
Verification , Formal Methods , Compiler Optimizations, , Functional Programming , CakeML