版本更新 · v5arXiv:2505.07681更新于 2026-11-04Verified Purely Functional Catenable Real-Time DequesJules Viennot, Arthur Wendling, Armaël Guéneau, François Pottier原文摘要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.cs.PL · cs.DS · cs.LO