PureCake: Towards a formally verified non-strict language compiler

Typ
Examensarbete för masterexamen
Program
Computer systems and networks (MPCSN), MSc
Publicerad
2020
Författare
ZANETTI, RICCARDO
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
CakeML is an end-to-end formally verified compiler for a subset of the Standard ML language. Its provenly correct compilation chain prevents several classes of software bugs from seeping into the project, while drastically reducing the chances of many others to occur. In turn, other software projects can be built on top of CakeML; their correctness can be proven with respect to CakeML semantics, and ultimately produce software that is itself end-to-end verified. The aim of this thesis is to bring a pure non-strict language variant (PureCake) into the project. The peculiar properties of the language, which include purity, referen tial transparency and equational reasoning facilitate the proof process, ultimately encouraging the spread of formal methods.
Beskrivning
Ämne/nyckelord
compilers , formal verification , interactive theorem provers , functional programming , formal semantics of programming languages , code optimizations , inlining
Citation
Arkitekt (konstruktör)
Geografisk plats
Byggnad (typ)
Byggår
Modelltyp
Skala
Teknik / material
Index