[isabelle] New in the AFP: Root-Balanced Tree

Root-Balanced Tree
  by Tobias Nipkow

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.

More details at https://www.isa-afp.org/entries/Root_Balanced_Tree.html


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.