collaborators

1 paper

cs.PL2026

Verified Purely Functional Catenable Real-Time Deques

Jules Viennot, Arthur Wendling, Armaël Guéneau +1

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.