[isabelle] New in the AFP: Weight-Balanced Trees by Tobias Nipkow and Stefan Dirix
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] New in the AFP: Weight-Balanced Trees by Tobias Nipkow and Stefan Dirix
- From: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>
- Date: Tue, 13 Mar 2018 18:27:50 +0000
- Accept-language: de-DE, de-AT, en-US
- Thread-index: AQHTuvj9Lfqovwf5FUu1LuDzP+eovA==
- Thread-topic: New in the AFP: Weight-Balanced Trees by Tobias Nipkow and Stefan Dirix
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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and