arXiv:2505.07681 · v5

Verified Purely Functional Catenable Real-Time Deques

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

首次提交 2025-05-12 23:47

版本更新 2026-11-04 21:34

雷达观测 2026-11-05 12:13

摘要

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 原文 ↗阅读 PDF ↗

AI 论文解读

基于摘要 · 非全文审阅

此版本尚未生成 AI 解读。解读由后台任务生成并按论文版本保存，登录后共享已有结果。

版本差异

目前只观测到一个版本，无法比较变化。之后收录新版本时，会在这里对照标题、作者、分类和摘要。

观测到的版本

相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。

v5 · 2026-11-04 21:34 · 最新观测版本

Verified Purely Functional Catenable Real-Time Deques

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.

查看此版本解读 →查看此版本原文 ↗