# AVL Trees

 Title: AVL Trees Authors: Tobias Nipkow and Cornelia Pusch Submission date: 2004-03-19 Abstract: Two formalizations of AVL trees with room for extensions. The first formalization is monolithic and shorter, the second one in two stages, longer and a bit simpler. The final implementation is the same. If you are interested in developing this further, please contact gerwin.klein@nicta.com.au. Change history: [2011-04-11]: Ondrej Kuncar added delete function BibTeX: @article{AVL-Trees-AFP, author = {Tobias Nipkow and Cornelia Pusch}, title = {AVL Trees}, journal = {Archive of Formal Proofs}, month = mar, year = 2004, note = {\url{http://isa-afp.org/entries/AVL-Trees.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License