AVL Trees

Tobias Nipkow and Cornelia Pusch

19 March 2004

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.
BSD License

Change history

[2011-04-11] Ondrej Kuncar added delete function

Topics

Theories

Cite

×
@article{AVL-Trees-AFP,
  author  = {Tobias Nipkow and Cornelia Pusch},
  title   = {AVL Trees},
  journal = {Archive of Formal Proofs},
  month   = March,
  year    = 2004,
  note    = {\url{http://isa-afp.org/entries/AVL-Trees.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download