#rocqprover — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #rocqprover, aggregated by home.social.
-
Verification of a DPLL transition system in Rocq. ~ Julia Dijkstra, Benedikt Ahrens. https://arxiv.org/abs/2607.14999v1 #RocqProver #ITP
-
Verification of a DPLL transition system in Rocq. ~ Julia Dijkstra, Benedikt Ahrens. https://arxiv.org/abs/2607.14999v1 #RocqProver #ITP
-
Verification of a DPLL transition system in Rocq. ~ Julia Dijkstra, Benedikt Ahrens. https://arxiv.org/abs/2607.14999v1 #RocqProver #ITP
-
Verification of a DPLL transition system in Rocq. ~ Julia Dijkstra, Benedikt Ahrens. https://arxiv.org/abs/2607.14999v1 #RocqProver #ITP
-
Verification of a DPLL transition system in Rocq. ~ Julia Dijkstra, Benedikt Ahrens. https://arxiv.org/abs/2607.14999v1 #RocqProver #ITP
-
Verified purely functional catenable real-time deques. ~ Jules Viennot, Arthur Wendling, Armaël Guéneau, François Pottier. https://arxiv.org/abs/2505.07681 #RocqProver #ITP #FunctionalProgramming
-
Verified purely functional catenable real-time deques. ~ Jules Viennot, Arthur Wendling, Armaël Guéneau, François Pottier. https://arxiv.org/abs/2505.07681 #RocqProver #ITP #FunctionalProgramming
-
I understand that there are editorial conventions for this, and I would like my opinion on the matter to be known, to wit:
1. Those editorial conventions are wrong, and
2. If I read this in an article, I will assume that the writer pronounces it "a mhll language." -
Extraction and search in Rocq: Theorems, definitions and their dependencies. ~ Jian Fang, Yingfei Xiong. https://arxiv.org/abs/2606.04704v1 #RocqProver #ITP
-
Extraction and search in Rocq: Theorems, definitions and their dependencies. ~ Jian Fang, Yingfei Xiong. https://arxiv.org/abs/2606.04704v1 #RocqProver #ITP
-
Putnam 2025 problems in Rocq using Opus 4.6 and Rocq-MCP. ~ Guillaume Baudart, Marc Lelarge, Tristan Stérin, Jules Viennot. https://arxiv.org/abs/2603.20405 #AI4Math #RocqProver
-
Putnam 2025 problems in Rocq using Opus 4.6 and Rocq-MCP. ~ Guillaume Baudart, Marc Lelarge, Tristan Stérin, Jules Viennot. https://arxiv.org/abs/2603.20405 #AI4Math #RocqProver
-
Four–in-a-row in Rocq. ~ Laurent Théry. https://inria.hal.science/hal-05625464/document #RocqProver #ITP
-
Four–in-a-row in Rocq. ~ Laurent Théry. https://inria.hal.science/hal-05625464/document #RocqProver #ITP
-
TableauxRocq: A deep embedding of free-variable tableaux in Rocq. ~ Johann Rosain, Julie Cailler. https://arxiv.org/abs/2605.16952v1 #RocqProver #ITP
-
TableauxRocq: A deep embedding of free-variable tableaux in Rocq. ~ Johann Rosain, Julie Cailler. https://arxiv.org/abs/2605.16952v1 #RocqProver #ITP
-
**Rocq’n’Share 2026**
**Jun 29–Jul 3, EPFL**
Registration free but required: https://framaforms.org/rocqnshare-2026-registration-1769966293
More details: https://proofs.swiss/rocq-n-share/2026/Are you itching to learn more about the internals of your favorite proof assistant? Do you have a feature to advocate for? Do you need help implementing an extension or hacking the kernel? Do you feel ready to step up and fix that bug that's been pestering you for years?
Join us for Rocq’n’Share! (contd. in thread)
-
It’s neat to see that an old (fiddly, complicated) decidability argument I wrote up in the 1990s is getting some attention. Here, Raj Goré and Anthony Peigné formalise (and generalise) my decidability argument for display formulations of some substructural logics. This is interesting work, worth looking into.
https://link.springer.com/article/10.1007/s11225-026-10239-8
-
It’s neat to see that an old (fiddly, complicated) decidability argument I wrote up in the 1990s is getting some attention. Here, Raj Goré and Anthony Peigné formalise (and generalise) my decidability argument for display formulations of some substructural logics. This is interesting work, worth looking into.
https://link.springer.com/article/10.1007/s11225-026-10239-8
-
A general formalised framework for reasoning about display calculi. ~ Rajeev Goré, Anthony Peigné. https://link.springer.com/article/10.1007/s11225-026-10239-8 #RocqProver #ITP #Logic
-
A general formalised framework for reasoning about display calculi. ~ Rajeev Goré, Anthony Peigné. https://link.springer.com/article/10.1007/s11225-026-10239-8 #RocqProver #ITP #Logic
-
A formal proof of the Sands-Sauer-Woodrow theorem using the Rocq prover and mathcomp/ssreflect. ~ Jean-Philippe Chancelier. https://arxiv.org/abs/2604.21376 #RocqProver #ITP #Math
-
A formal proof of the Sands-Sauer-Woodrow theorem using the Rocq prover and mathcomp/ssreflect. ~ Jean-Philippe Chancelier. https://arxiv.org/abs/2604.21376 #RocqProver #ITP #Math
-
On reasoning-centric LLM-based automated theorem proving. ~ Yican Sun, Chengwei Shi, Hangzhou Lyu, Yingfei Xiong. https://arxiv.org/abs/2604.19558v1 #RocqProver #AI4Math
-
On reasoning-centric LLM-based automated theorem proving. ~ Yican Sun, Chengwei Shi, Hangzhou Lyu, Yingfei Xiong. https://arxiv.org/abs/2604.19558v1 #RocqProver #AI4Math
-
A Rocq formalization of simplicial Lagrange finite elements. ~ Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine. https://arxiv.org/abs/2604.20345v1 #RocqProver #ITP #Math
-
A Rocq formalization of simplicial Lagrange finite elements. ~ Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine. https://arxiv.org/abs/2604.20345v1 #RocqProver #ITP #Math
-
A constructive proof of Rice's theorem and the halting problem via Hilbert's tenth problem. ~ Jonathan Brossard. https://arxiv.org/abs/2604.16477v1 #RocqProver #ITP #Math
-
A constructive proof of Rice's theorem and the halting problem via Hilbert's tenth problem. ~ Jonathan Brossard. https://arxiv.org/abs/2604.16477v1 #RocqProver #ITP #Math
-
CARVe in Rocq: A library for substructural meta-theory. ~ Daniel Zackon et als. https://momigliano.di.unimi.it/papers/itp26.pdf #RocqProver #ITP