Root Balanced Tree swMATH ID: 28657 Software Authors: Tobias Nipkow Description: Root-Balanced Tree. Andersson introduced general balanced trees, search trees based on the design principle of partial rebuilding: perform update operations naively until the tree becomes too unbalanced, at which point a whole subtree is rebalanced. This article defines and analyzes a functional version of general balanced trees, which we call root-balanced trees. Using a lightweight model of execution time, amortized logarithmic complexity is verified in the theorem prover Isabelle. This is the Isabelle formalization of the material decribed in the APLAS 2017 article Verified Root-Balanced Trees by the same author, which also presents experimental results that show competitiveness of root-balanced with AVL and red-black trees. Homepage: https://www.isa-afp.org/entries/Root_Balanced_Tree.html Dependencies: Isabelle Related Software: Isabelle/HOL; Archive Formal Proofs; HOL; Isabelle; Amortized Complexity; Coq; Density Compiler; Random BSTs; Treaps; QuickSort Cost; CryptHOL; Ergodic theory; Poly/ML; Probabilistic_Prime_Tests; Monad normalisation; Quicksort; Verified LLL; LLL Factorization; Berlekamp Zassenhaus; Locales Cited in: 5 Documents all top 5 Cited by 9 Authors 4 Nipkow, Tobias 3 Haslbeck, Max W. 2 Eberl, Manuel 1 Bottesch, Ralph Christian 1 Brinkop, Hauke 1 Divasón, Jose 1 Joosten, Sebastiaan J. C. 1 Thiemann, René 1 Yamada, Akihisa Cited in 1 Serial 3 Journal of Automated Reasoning Cited in 2 Fields 5 Computer science (68-XX) 1 Number theory (11-XX) Citations by Year