Optimizing Stack Allocation for the CakeML Compiler
| dc.contributor.author | Ahlin, Richard | |
| 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 | Schneider, Gerardo | |
| dc.contributor.supervisor | Myreen, Magnus | |
| dc.date.accessioned | 2023-11-06T12:43:31Z | |
| dc.date.available | 2023-11-06T12:43:31Z | |
| dc.date.issued | 2023 | |
| dc.date.submitted | 2023 | |
| dc.description.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. | |
| dc.identifier.coursecode | DATX05 | |
| dc.identifier.uri | http://hdl.handle.net/20.500.12380/307320 | |
| dc.language.iso | eng | |
| dc.setspec.uppsok | Technology | |
| dc.subject | Verification | |
| dc.subject | Formal Methods | |
| dc.subject | Compiler Optimizations, | |
| dc.subject | Functional Programming | |
| dc.subject | CakeML | |
| dc.title | Optimizing Stack Allocation for the CakeML 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 |