HackerPapers

arXiv:2505.07681cs.PL

Verified Purely Functional Catenable Real-Time Deques

Jules Viennot, Arthur Wendling, Armaël Guéneau, François Pottier

HN submission. Found in a submission link or body. Submitters do not count as commenters in the main ranking; a submission is not an endorsement.

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 comments
Journal reference
DOI
Subjects
cs.PLProgramming Languages cs.DSData Structures and Algorithms cs.LOLogic in Computer Science

On Hacker News

No comments linking this paper were found in the collected sources. Found in 1 HN submission from May 2025 to May 2025. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments0 threads

No comments linking this paper were found in the collected sources. Open submission discussions.

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.