AVL Trees

Tobias Nipkow 🌐 and Cornelia Pusch

March 19, 2004

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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


April 11, 2011
Ondrej Kuncar added delete function


Session AVL-Trees