Improving Memory Consumption with FAITH - a Proof Assistant for Improvement Theory
Ladda ner
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