Verified Function Inlining Optimization fro the PureCake 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
Korban, Kacper
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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.
Beskrivning
Ämne/nyckelord
Formal Methods , Functional Programming , Formal Verification , Programming Languages , Compilers