MiniF2F in Rocq: Automatic Translation Between Proof Assistants - A Case Study. - Jules Viennot; Guillaume Baudart; Emilio Jesús Gallego Arias; Marc Lelarge (CoRR, 2025)

Verified Purely Functional Catenable Real-Time Deques. - Jules Viennot; Arthur Wendling; Armaël Guéneau; François Pottier (CoRR, 2025)