Proofs of Data

Verified functional data structures with LiquidHaskell.

Inspired by Andrew Appel's Verified Functional Algorithms.

Chapter dependencies

- Perm  -> Sort  -> Selection  -> SearchTree -> Redblack
  |        |                      |
  `->Trie  `-> Multiset           `-> ADT -> Priqueue -> Binom

Issues

• RedBlack hammers PLE-SLOW

Progress

• Perm
• Sort
• Multiset
• Selection
• TotalMaps
• SearchTree
• Trie
• [-] ADT
• Priqueue
• Binom <--------------------------- HEREHEREHEREHEREHEREHERE
• RedBlack