#rocqprover — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #rocqprover, aggregated by home.social.
-
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
-
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
-
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 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 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
-
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
-
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
-
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
-
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 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 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
-
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