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

1 Abstract

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.

2 Report

3 Code

4 Talk

5 Revised code

6 Also see

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.

Author: Linus Ek, Ola Holmström and Stevan Andjelkovic <{linek,olahol,stevan}>

Date: 2011-05-08 14:49:30 CEST