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定理证明器中的嵌入进行了形式化机械化。