Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Weight-Balanced Trees by Tobia...

Email Gateway (Aug 22 2022 at 16:56):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear all,

today there is a nice new entry by Tobias Nipkow and Stefan Dirix.
It is on weight-balanced trees, a topic on which there are previous
papers containing wrong claims.

Enjoy,
René

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.

Last updated: Apr 20 2024 at 04:19 UTC