Agda2hs is a program which compiles a subset of Agda to Haskell. In this paper, an implementation of the Haskell library QuadTree is created and verified in this subset of Agda, such that Agda2hs can then produce a verified Haskell implementation. To aid with this verification, a number of techniques have been proposed which are used to prove invariants, preconditions and post-conditions of the QuadTree library. Using these techniques, the properties of the library have been proven. Additionally, recommendations are made to reduce the time needed for verification. The full paper is available here.
Each directory in the sources has an explanation as to what each file is for. Click here to start exploring!
- Make sure Haskell and Agda are installed via Stack
- Download and install my fork of agda2hs, available at https://github.com/JonathanBrouwer/agda2hs (This compiles Nats in a different way)
git clone https://github.com/JonathanBrouwer/research-project.gitcd research-projectmake(no arguments to the make needed)- It should now have compiled all agda files to haskell
- To run Haskell quickcheck, run
stack test