Proof Pearl: Braun Trees
Braun trees are functional data structures for implementing extensible
arrays and priority queues (and sorting functions based on the latter)
efficiently. Some well-known functions on Braun trees have not yet
been verified, including especially Okasaki's linear time conversion
from lists to Braun trees. We supply the missing proofs and verify all
of these algorithms in Isabelle, including non-obvious time
complexity claims. In particular we provide the first linear-time
conversion from Braun trees to lists. We also state and verify a new
characterization of Braun trees as the trees t whose index set is the
interval {1, ..., size of t}.
Latest version: pdf
Official published version: pdf
BibTeX:
@inproceedings{NipkowS-CPP20,
author={Tobias Nipkow and Thomas Sewell},
title={Proof Pearl: Braun Trees},
booktitle={Certified Programs and Proofs, {CPP} 2020},
editor={J. Blanchette and C. Hritcu},
publisher={ACM},pages={18-31},year=2020}
Isabelle theories:
Isabelle Distribution
AFP