Arboretum
A place where to play (mainly) with some trees.
Reading list
- Quicksort in Idris
- Decidable Orderings in Idris
- InsertionSort in Idris
- Verified BST Idris
- Verifying Data Structures in Haskell (post)
- Verifying Data Structures in Haskell (code)
- Verified AVLs in Haskell (post)
- Verified AVLs in Haskell (code)
- Proving that merging two sorted lists produces a sorted list
Bibliography
- Okasaki, Chris. (1999). Functional Pearls: Red-Black Trees in a Functional Setting. Journal of Functional Programming, 9 (4), 471-477
- Kahrs, Stefan. (2001). Functional Pearls: Red-Black Trees with Types. Journal of Functional Programming, 11 (4), 425-432
- McBride, Conor. (2014). How to keep your neighbours in order. ACM SIGPLAN Notices, 49 (9), 297-309