Verified Purely Functional Catenable Real-Time Deques
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909980560457728 |
|---|---|
| author | Viennot, Jules Wendling, Arthur Guéneau, Armaël Pottier, François |
| author_facet | Viennot, Jules Wendling, Arthur Guéneau, Armaël Pottier, François |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_07681 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Verified Purely Functional Catenable Real-Time Deques Viennot, Jules Wendling, Arthur Guéneau, Armaël Pottier, François Programming Languages Data Structures and Algorithms Logic in Computer Science 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. |
| title | Verified Purely Functional Catenable Real-Time Deques |
| topic | Programming Languages Data Structures and Algorithms Logic in Computer Science |
| url | https://arxiv.org/abs/2505.07681 |