Improving Memory Consumption with FAITH - a Proof Assistant for Improvement Theory

Visa enkel post
dc.contributor.authorSunnerhagen, Örjan
dc.contributor.departmentChalmers tekniska högskola / Institutionen för data och informationstekniksv
dc.contributor.examinerHughes, John
dc.contributor.supervisorSands, David
dc.date.accessioned2021-07-06T06:35:28Z
dc.date.available2021-07-06T06:35:28Z
dc.date.issued2021sv
dc.date.submitted2020
dc.description.abstractIn functional languages with lazy evaluation and sharing, such as Haskell, it is hard to reason about space usage. In particular, it is hard to know if a given local transformation in such a language will introduce an asymptotic space increase. Gustavsson and Sands have developed Space Improvement Theory to prove if such transformations introduced asymptotic space increase. However, since the proofs are long and complicated, Space Improvement proofs done on paper are prone to errors. To tackle this problem, I have constructed FAITH, the proof assistant for Improvement Theory. FAITH allows users to define transformational laws, such as those for Space Improvement, and then use those laws in proofs that transform one term to another step by step. In case of errors, FAITH provides helpful error messages. The main contributions of FAITH is to check proofs of inequational reasoning with custom transformational laws that can be applied inside arbitrary contexts. Keywords:sv
dc.identifier.urihttps://hdl.handle.net/20.500.12380/303634
dc.language.isoengsv
dc.setspec.uppsokTechnology
dc.subjectComputer Sciencesv
dc.subjectHaskellsv
dc.subjectoptimizationsv
dc.subjectperformancesv
dc.subjectfunctional programmingsv
dc.subjectformal verificationsv
dc.subjectproof assistantsv
dc.subjectImprovement Theorysv
dc.subjectmemory consumptionsv
dc.subjectSpace Improvement Theorysv
dc.titleImproving Memory Consumption with FAITH - a Proof Assistant for Improvement Theorysv
dc.type.degreeExamensarbete för masterexamensv
dc.type.uppsokH
Ladda ner
Original bundle
Visar 1 - 1 av 1
Bild (thumbnail)
Namn:
CSE 21-103 Sunnerhagen.pdf
Storlek:
1.34 MB
Format:
Adobe Portable Document Format
Beskrivning:
Ladda ner
License bundle
Visar 1 - 1 av 1
Bild (thumbnail)
Namn:
license.txt
Storlek:
1.51 KB
Format:
Item-specific license agreed upon to submission
Beskrivning:
Ladda ner
Samling
Examensarbeten för masterexamen