Verified Purely Functional Catenable Real-Time Deques
Jules Viennot, Arthur Wendling, Arma\"el Gu\'eneau, Fran\c{c}ois Pottier
TL;DR
This paper introduces verified implementations of purely functional, real-time catenable deques in OCaml and Rocq, with machine-checked correctness for the Rocq version, advancing reliable functional data structures.
Contribution
It provides the first verified implementations of these data structures in functional programming languages, ensuring correctness through formal methods.
Findings
Machine-checked correctness of Rocq implementation
Practical OCaml implementation of catenable deques
Advancement in verified functional data structures
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Distributed systems and fault tolerance