2023/09/20 by Runming Li, Li, Runming, Harrison Grodin +3 · 1 citation
Computer Science · #Advanced Graph Theory Research #Algorithms and Data Compression #Data Structures and Algorithms (cs.DS) #FOS: Computer and information sciences #Programming Languages (cs.PL) #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2309.11056
openalex publication_date 2023/09/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Ordered sequences of data, specified with a join operation to combine sequences, serve as a foundation for the implementation of parallel functional algorithms. This abstract data type can be elegantly and efficiently implemented using balanced binary trees, where a join operation is provided to combine two trees and rebalance as necessary. In this work, we present a verified implementation and cost analysis of joinable red-black trees in calf, a dependent type theory for cost analysis. We implement red-black trees and auxiliary intermediate data structures in such a way that all correctness invariants are intrinsically maintained. Then, we describe and verify precise cost bounds on the operations, making use of the red-black tree invariants. Finally, we implement standard algorithms on sequences using the simple join-based signature and bound their cost in the case that red-black trees are used as the underlying implementation. All proofs are formally mechanized using the embedding of calf in the Agda theorem prover.