We present a correct proof of Adams' trees of bounded balance, which are used in
Haskell to implement Data.Map and Data.Set. Our
analysis includes the previously ignored join operation, and also
guarantees trees with smaller depth than the original one. Because the Adams'
trees can be parametrized, we use benchmarking to find the best choice of
parameters. Finally, a saving memory technique based on introducing additional
data constructor is evaluated.
The paper was accepted to TFP 2011. The draft paper is available as PDF.
The detailed results of the benchmark are available here. All source code used is available as benchmark.tar.gz.