Verified Root-Balanced Trees
Abstract elided by the publisher.
Related papers
- The Functional Essence of Imperative Binary Search Trees PLDI 2024
- Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic CPP 2024
- Verifying concurrent multicopy search structures OOPSLA 2021
- The third homomorphism theorem on trees: downward & upward lead to divide-and-conquer POPL 2009
- Balancing weight-balanced trees JFP 2011
- Concurrent Balanced Augmented Trees PPoPP 2026
- Balanced trees inhabiting functional parallel programming ICFP 2011
- Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report) ICFP 2018