PureCake: Towards a formally verified non-strict language compiler
Ladda ner
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