The Functional Essence of Imperative Binary Search Trees
summary
Functional algorithms introduce a new first-class constructor context primitive and use Koka’s reuse-aware reference counting to implement tail-call, in-place partitioning for move-to-root, splay and zip trees. The paper mechanises equivalence between the functional and imperative versions in Coq mechanisation with Iris, yielding the first fully verified implementations of these restructuring BSTs. Benchmarks show performance on par with C (within a few percent; C edges when allocator differences are equalised). Artifacts and proofs are available.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:50Efficient functional trees
- 2:32Move-to-root trees
- 5:45Stack inefficiency
- 6:08Constructor contexts
- 8:56Constructor contexts in practice
- 10:42Full algorithm
- 11:25Verifying algorithms
- 13:09Performance comparison
- 13:50Limitations and future work
- 14:11Conclusion
- 14:32Q&A
related talks
24mChoice Trees: Representing Nondeterministic, Recursive, and Impure Programs in C...
15mSealing Pointer-Based Optimizations Behind Pure Functions
21mBonsai: Compiling Queries to Pruned Tree Traversals
32mTyped Program Analysis Without Encodings
01h 47mFunctional C++
30mComputation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
35mOutperforming Imperative with Pure Functional Languages
08mCompiling pattern matching to in-place modifications