Julien Oster: An Agda Implementation of Deletion in Left-leaning Red-Black Trees
TCS Oberseminar, 10.12.2010, 14:15
Julien Oster, An Agda implementation of deletion in Left-leaning Red-Black trees
We present an implementation of deletion in Left-leaning Red-Black-trees in Literate Agda, based on a modified data structure originally by Ek, Holmström and Andjelkovic, and explain in detail how Agda ensures correctness by definition of the algorithm.
Artikelaktionen
abgelegt unter:
Oberseminar