Formalizing Arne Andersson trees and Left-leaning Red-Black trees in Agda

We will show how to use the dependently typed programming language, Agda, to prove the binary search tree invariant of Arne Andersson trees and the binary search tree and the color invariants of Left-leaning Red-Black trees under insertion. We do not prove that the bag of elements in the tree insert(a, t) is equal to the bag of elements in t with the element a added.

May 19, 2009 (PDF)

Sorted lists
Ulf Norell's 2-3 trees
Arne Andersson trees
Left-leaning red-black trees in Haskell
Left-leaning red-black trees in Agda

June 10, 2009 (PDF)

Left-leaning red-black trees (June 17, 2009)

Julien Oster at Ludwig-Maximilians-Universität in München has, under the supervision of Andreas Abel, implemented deletion for Left-leaning Red-Black trees in Agda. The report can be found here and the code here.