#rocq — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #rocq, aggregated by home.social.
-
**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)
-
TIL the the expression whose value is being "scrutinized" in a pattern match (in #Rocq) is called "scrutinee".
-
I wrote my first 1000 lines of code of #rocq
I’m impressed that I have just scratched the surface of it. -
Is anyone going here this weekend? Agda is one of the most innovative game changers in functional programming and theorem proving, given its unique implementation architecture and capabilities. I'd like to meet you there! π🐫λ #CubicalAgda #Rocq #OCaml #Haskell types2026.cse.chalmers.se
TYPES 2026: TYPES 2026 -
Yeeee, I completed chapter 1 (of 17) of volume 1 (of 7) of Software Foundation.
It's a long way to the top if you wanna #Rocq and roll.
-
🚀 Behold the renaming of #Coq to #Rocq, as if the world needed another rocq-solid theorem prover to prove how uselessly rocq-hard #math can be. 🤔 But wait, there's more! Now with extra Polymorphic, Cumulative Calculus of Inductive Constructions, because everyone clearly needs that in their morning coffee. ☕📚
https://rocq-prover.org/about #TheoremProver #Humor #PolymorphicCalculus #HackerNews #ngated -
🚀 Behold the renaming of #Coq to #Rocq, as if the world needed another rocq-solid theorem prover to prove how uselessly rocq-hard #math can be. 🤔 But wait, there's more! Now with extra Polymorphic, Cumulative Calculus of Inductive Constructions, because everyone clearly needs that in their morning coffee. ☕📚
https://rocq-prover.org/about #TheoremProver #Humor #PolymorphicCalculus #HackerNews #ngated -
🚀 Behold the renaming of #Coq to #Rocq, as if the world needed another rocq-solid theorem prover to prove how uselessly rocq-hard #math can be. 🤔 But wait, there's more! Now with extra Polymorphic, Cumulative Calculus of Inductive Constructions, because everyone clearly needs that in their morning coffee. ☕📚
https://rocq-prover.org/about #TheoremProver #Humor #PolymorphicCalculus #HackerNews #ngated -
🚀 Behold the renaming of #Coq to #Rocq, as if the world needed another rocq-solid theorem prover to prove how uselessly rocq-hard #math can be. 🤔 But wait, there's more! Now with extra Polymorphic, Cumulative Calculus of Inductive Constructions, because everyone clearly needs that in their morning coffee. ☕📚
https://rocq-prover.org/about #TheoremProver #Humor #PolymorphicCalculus #HackerNews #ngated -
🚀 Behold the renaming of #Coq to #Rocq, as if the world needed another rocq-solid theorem prover to prove how uselessly rocq-hard #math can be. 🤔 But wait, there's more! Now with extra Polymorphic, Cumulative Calculus of Inductive Constructions, because everyone clearly needs that in their morning coffee. ☕📚
https://rocq-prover.org/about #TheoremProver #Humor #PolymorphicCalculus #HackerNews #ngated -
Coq theorem prover is now called Rocq
#HackerNews #Coq #Rocq #theorem #prover #programming #languages #proof #assistants
-
Coq theorem prover is now called Rocq
#HackerNews #Coq #Rocq #theorem #prover #programming #languages #proof #assistants
-
Coq theorem prover is now called Rocq
#HackerNews #Coq #Rocq #theorem #prover #programming #languages #proof #assistants
-
Coq theorem prover is now called Rocq
#HackerNews #Coq #Rocq #theorem #prover #programming #languages #proof #assistants
-
Coq theorem prover is now called Rocq
#HackerNews #Coq #Rocq #theorem #prover #programming #languages #proof #assistants
-
Our department is hiring an assistant professor in computer science (including programming languages). If you would like to join our small but diverse PL group in beautiful little Delft, please don't hesitate to apply! Also feel free to reach out to me if you want to know anything about our department or academic life in the Netherlands.
Deadline for applications: 11th of May
academictransfer.com/en/jobs/360114/assistant-professor-in-computer-science/
#TUDelft #AssistantProfessor #Hiring #ComputerScience #SoftwareTechnology #ProgrammingLanguages #TypeTheory #SoftwareVerification #Agda #Rocq -
Our department is hiring an assistant professor in computer science (including programming languages). If you would like to join our small but diverse PL group in beautiful little Delft, please don't hesitate to apply! Also feel free to reach out to me if you want to know anything about our department or academic life in the Netherlands.
Deadline for applications: 11th of May
academictransfer.com/en/jobs/360114/assistant-professor-in-computer-science/
#TUDelft #AssistantProfessor #Hiring #ComputerScience #SoftwareTechnology #ProgrammingLanguages #TypeTheory #SoftwareVerification #Agda #Rocq -
Our department is hiring an assistant professor in computer science (including programming languages). If you would like to join our small but diverse PL group in beautiful little Delft, please don't hesitate to apply! Also feel free to reach out to me if you want to know anything about our department or academic life in the Netherlands.
Deadline for applications: 11th of May
academictransfer.com/en/jobs/360114/assistant-professor-in-computer-science/
#TUDelft #AssistantProfessor #Hiring #ComputerScience #SoftwareTechnology #ProgrammingLanguages #TypeTheory #SoftwareVerification #Agda #Rocq -
Our department is hiring an assistant professor in computer science (including programming languages). If you would like to join our small but diverse PL group in beautiful little Delft, please don't hesitate to apply! Also feel free to reach out to me if you want to know anything about our department or academic life in the Netherlands.
Deadline for applications: 11th of May
academictransfer.com/en/jobs/360114/assistant-professor-in-computer-science/
#TUDelft #AssistantProfessor #Hiring #ComputerScience #SoftwareTechnology #ProgrammingLanguages #TypeTheory #SoftwareVerification #Agda #Rocq -
Our department is hiring an assistant professor in computer science (including programming languages). If you would like to join our small but diverse PL group in beautiful little Delft, please don't hesitate to apply! Also feel free to reach out to me if you want to know anything about our department or academic life in the Netherlands.
Deadline for applications: 11th of May
academictransfer.com/en/jobs/360114/assistant-professor-in-computer-science/
#TUDelft #AssistantProfessor #Hiring #ComputerScience #SoftwareTechnology #ProgrammingLanguages #TypeTheory #SoftwareVerification #Agda #Rocq -
-
Cylindrical algebraic decomposition in Coq/Rocq. ~ Quentin Vermande. https://dl.acm.org/doi/pdf/10.1145/3779031.3779100 #ITP #Rocq
-
Readings shared December 29, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/30-readings_shared_12-29-25 #AI #Agda #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #OCaml #Rocq #SMT
-
Tacq: Context aware tactic recommendation for Rocq. ~ Jules Viennot, Guillaume Baudart, Emilio Jesús Gallego Arias, Marc Lelarge, Theo Stoskopf. https://hal.science/hal-05428166/document#page=205 #ITP #Rocq
-
Formalisation de la stabilité de l’erreur d’estimation de l’inclinaison d’un robot. ~ Lynda Bentoucha, Reynald Affeldt. https://hal.science/hal-05428166/document#page=194 #ITP #Rocq
-
Une sémantique de Kahn mécanisée pour les machines à états. ~ Timothy Bourke, Paul Jeanmaire, Marc Pouzet. https://hal.science/hal-05428166/document#page=17 #ITP #Rocq
-
Formal verification of Borrow-Checking by local commutation diagrams. ~ Alban Reynaud Michez. https://hal.science/hal-05428143/ #ITP #Rocq
-
The machine-checked complete formalization of Landau’s foundations of analysis in Rocq. ~ Yue Guan, Yaoshun Fu, Xiangtao Meng. https://www.mdpi.com/2227-7390/14/1/61 #ITP #Rocq #Math
-
Readings shared December 19, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/20-readings_shared_12-19-25 #AI #ITP #IsabelleHOL #LLMs #LeanProver #Math #Rocq
-
Prediction: AI will make formal verification go mainstream. ~ Martin Kleppmann. https://martin.kleppmann.com/2025/12/08/ai-formal-verification.html #AI #LLMs #ITP #LeanProver #IsabelleHOL #Rocq
-
A rose tree is blooming (Proof Pearl). ~ Joomy Korkut. https://joomy.korkutblech.com/papers/game-trees-cpp26.pdf #ITP #Rocq
-
Readings shared December 5, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/06-readings_shared_12-05-25 #ATP #Autoformalization #DataScience #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Rocq #Rstats #SMT #Z3
-
Readings shared December 5, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/06-readings_shared_12-05-25 #ATP #Autoformalization #DataScience #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Rocq #Rstats #SMT #Z3
-
Readings shared December 5, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/06-readings_shared_12-05-25 #ATP #Autoformalization #DataScience #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Rocq #Rstats #SMT #Z3
-
Readings shared December 5, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/06-readings_shared_12-05-25 #ATP #Autoformalization #DataScience #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Rocq #Rstats #SMT #Z3
-
Readings shared December 5, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/06-readings_shared_12-05-25 #ATP #Autoformalization #DataScience #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Rocq #Rstats #SMT #Z3
-
A Rocq formalization of monomial and graded orders. ~ Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero. https://arxiv.org/abs/2512.04573 #ITP #Rocq #Math
-
Readings shared December 2, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/03-readings_shared_12-02-25 #AI #CoqProver #ITP #IsabelleHOL #LLMs #LeanProver #Math #Rocq
