We present OCaml and Rocq implementations of Kaplan and Tarjan's purely functional, real-time catenable deques. The correctness of our Rocq implementation is machine-checked.

翻译：我们实现了Kaplan和Tarjan提出的纯函数式实时可连接双端队列的OCaml和Rocq版本。其中Rocq实现的正确性通过了机器验证。