Verified Function Inlining Optimization fro the PureCake Compiler
| dc.contributor.author | Korban, Kacper | |
| dc.contributor.department | Chalmers tekniska högskola / Institutionen för data och informationsteknik | sv |
| dc.contributor.department | Chalmers University of Technology / Department of Computer Science and Engineering | en |
| dc.contributor.examiner | Sheeran, Mary | |
| dc.contributor.supervisor | Myreen, Magnus | |
| dc.date.accessioned | 2023-06-21T11:39:12Z | |
| dc.date.available | 2023-06-21T11:39:12Z | |
| dc.date.issued | 2023 | |
| dc.date.submitted | 2023 | |
| dc.description.abstract | 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. | |
| dc.identifier.uri | http://hdl.handle.net/20.500.12380/306357 | |
| dc.setspec.uppsok | Technology | |
| dc.subject | Formal Methods | |
| dc.subject | Functional Programming | |
| dc.subject | Formal Verification | |
| dc.subject | Programming Languages | |
| dc.subject | Compilers | |
| dc.title | Verified Function Inlining Optimization fro the PureCake Compiler | |
| dc.type.degree | Examensarbete för masterexamen | sv |
| dc.type.degree | Master's Thesis | en |
| dc.type.uppsok | H | |
| local.programme | Computer science – algorithms, languages and logic (MPALG), MSc |