AVL Trees

Tobias Nipkow 🌐 and Cornelia Pusch

March 19, 2004


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

April 11, 2011

Ondrej Kuncar added delete function


Theories of AVL-Trees