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 $\textbf{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 $\textbf{calf}$ in the Agda theorem prover.

翻译：使用连接操作组合序列的有序数据序列，为并行函数式算法的实现提供了基础。这种抽象数据类型可以通过平衡二叉树优雅高效地实现，其中提供连接操作以合并两棵树并在必要时重新平衡。在本工作中，我们针对可连接红黑树，在一种用于代价分析的依赖类型理论 $\textbf{calf}$ 中，提出了验证性实现和代价分析。我们以所有正确性不变量均内在保持的方式实现了红黑树及辅助中间数据结构。随后，我们利用红黑树不变量，描述并验证了操作的精确保留时间界限。最后，我们使用基于连接的简单签名在序列上实现标准算法，并在以红黑树作为底层实现时限定其代价。所有证明均借助 $\textbf{calf}$ 在 Agda 定理证明器中的嵌入性进行了形式化机械化。