[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. 


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.