Weight-Balanced Trees


Title: Weight-Balanced Trees
Authors: Tobias Nipkow and Stefan Dirix
Submission date: 2018-03-13
Abstract: This theory provides a verified implementation of weight-balanced trees following the work of Hirai and Yamamoto who proved that all parameters in a certain range are valid, i.e. guarantee that insertion and deletion preserve weight-balance. Instead of a general theorem we provide parameterized proofs of preservation of the invariant that work for many (all?) valid parameters.
  author  = {Tobias Nipkow and Stefan Dirix},
  title   = {Weight-Balanced Trees},
  journal = {Archive of Formal Proofs},
  month   = mar,
  year    = 2018,
  note    = {\url{https://isa-afp.org/entries/Weight_Balanced_Trees.html},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.