Verified Purely Functional Catenable Real-Time Deques
arXiv:2505.07681
Abstract
We present OCaml and Rocq implementations of Kaplan and Tarjan's purely functional, real-time catenable deques. The correctness of our Rocq code is machine-checked.
arXiv:2505.07681
We present OCaml and Rocq implementations of Kaplan and Tarjan's purely functional, real-time catenable deques. The correctness of our Rocq code is machine-checked.