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.
cs.PL↗
arXiv subjects
Armaël Guéneau
Publications and source records attributed to Armaël Guéneau.
The ins and outs of iteration in Mezzo
This is a talk proposal for HOPE 2013. Using iteration over a collection as a case study, we wish to illustrate the strengths and weaknesses of the prototype programming language Mezzo.
cs.PL↗