[isabelle] New in the AFP: Weight-Balanced Trees by Tobias Nipkow and Stefan Dirix



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.


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