PureCake: Towards a formally verified non-strict language compiler

dc.contributor.authorZANETTI, RICCARDO
dc.contributor.departmentChalmers tekniska högskola / Institutionen för data och informationstekniksv
dc.contributor.examinerHughes, John
dc.contributor.supervisorMyreen, Magnus
dc.date.accessioned2021-04-23T09:04:38Z
dc.date.available2021-04-23T09:04:38Z
dc.date.issued2020sv
dc.date.submitted2020
dc.description.abstractCakeML 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.sv
dc.identifier.coursecodeMPALGsv
dc.identifier.urihttps://hdl.handle.net/20.500.12380/302318
dc.language.isoengsv
dc.setspec.uppsokTechnology
dc.subjectcompilerssv
dc.subjectformal verificationsv
dc.subjectinteractive theorem proverssv
dc.subjectfunctional programmingsv
dc.subjectformal semantics of programming languagessv
dc.subjectcode optimizationssv
dc.subjectinliningsv
dc.titlePureCake: Towards a formally verified non-strict language compilersv
dc.type.degreeExamensarbete för masterexamensv
dc.type.uppsokH
local.programmeComputer systems and networks (MPCSN), MSc
Ladda ner
Original bundle
Visar 1 - 1 av 1
Hämtar...
Bild (thumbnail)
Namn:
CSE 21-10 Zanetti.pdf
Storlek:
356.05 KB
Format:
Adobe Portable Document Format
Beskrivning:
License bundle
Visar 1 - 1 av 1
Hämtar...
Bild (thumbnail)
Namn:
license.txt
Storlek:
1.14 KB
Format:
Item-specific license agreed upon to submission
Beskrivning: