PureCake: Towards a formally verified non-strict language compiler

Abstract

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.