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
  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