首页|Verified Purely Functional Catenable Real-Time Deques

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 implementation is machine-checked.

作者：Jules Viennot、Arthur Wendling、Arma?l Guéneau、Fran?ois Pottier

作者单位：

学科分类：计算技术、计算机技术

推荐引用：Jules Viennot,Arthur Wendling,Arma?l Guéneau,Fran?ois Pottier.Verified Purely Functional Catenable Real-Time Deques[EB/OL].(2025-05-12)[2025-06-12].https://arxiv.org/abs/2505.07681.点此复制

Verified Purely Functional Catenable Real-Time Deques

Verified Purely Functional Catenable Real-Time Deques

评论