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

Typ
Examensarbete för masterexamen
Program
Publicerad
2021
Författare
Sunnerhagen, Örjan
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
In 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:
Beskrivning
Ämne/nyckelord
Computer Science, Haskell, optimization, performance, functional programming, formal verification, proof assistant, Improvement Theory, memory consumption, Space Improvement Theory
Citation
Arkitekt (konstruktör)
Geografisk plats
Byggnad (typ)
Byggår
Modelltyp
Skala
Teknik / material