Verified Purely Functional Catenable Real-Time Deques
Programming Languages
2026-01-06 v2 Data Structures and Algorithms
Logic in Computer Science
Abstract
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.
Cite
@article{arxiv.2505.07681,
title = {Verified Purely Functional Catenable Real-Time Deques},
author = {Jules Viennot and Arthur Wendling and Armaël Guéneau and François Pottier},
journal= {arXiv preprint arXiv:2505.07681},
year = {2026}
}