Formal verification gives us the obvious benefits of reducing errors and an increased trues in the proven system. However, formal verification of programs are not common-place and are mostly reserved for some special use cases.
Liquid Haskell [VJ14a] , a verifier for Haskell programs, tries to avoid these issues. With the use of refinement types and an SMT-solver, it tries to automate a lot of the verification.
In this thesis we investigate Liquid Haskell in two ways. Comparing it to the type level programming in Haskell, and also to verify properties of Finger trees.
| supervisor | Martin Steffen |
| IFI links | abstract, thesis, presentation |
| github | code repository |