Mastodawn

🚀 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

About The Rocq Prover

Rocq is a mature, dependently-typed functional programming language and interactive theorem prover. Learn more about its rich history.

Rocq

Hacker News 13h ago

Coq theorem prover is now called Rocq

https://rocq-prover.org/about

#HackerNews #Coq #Rocq #theorem #prover #programming #languages #proof #assistants

About The Rocq Prover

Rocq is a mature, dependently-typed functional programming language and interactive theorem prover. Learn more about its rich history.

Rocq

Jesper Agdakx 🔸4d ago

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

Assistant Professor in Computer Science

Develop the next generation of CS and AI intelligence technology that powers science and society at TU Delft. Combine research with real technological impact while educating talented students. Job description Are you inspired by shaping the next generation of…

AcademicTransfer

arialdo Apr 1

Current status: installed #rocq, reading Software Foundation.

Fraser Tweedale Mar 26

RE: https://functional.cafe/@hackuador/116282882755691464

Two more sleeps until the first #BFPG Hack Day of 2026! See yas there, curious minds!

#FP #Haskell #OCaml #Idris #Gleam #Lean #Scala #Erlang #Elixir #FSharp #Clojure #Lisp #Agda #Rocq #Rust #Scheme #Racket

Fraser Tweedale Mar 18

Thanks to Sirius-beta Labs who are once again sponsoring lunch for #BFPG Hack Day. UQ St Lucia, Saturday 28 March. Be there or be a lambda cube!

#FP #Haskell #OCaml #Idris #Gleam #Lean #Scala #Erlang #Elixir #FSharp #Clojure #Lisp #Agda #Rocq #Rust #Scheme #Racket

https://luma.com/uu28az9h

BFPG Hack Day - March 2026 · Luma

Come to BFPG Hack Day for some wholesome fun hacking on side projects, tackling tutorials, grinding axes and shaving yaks! Work together or independently.…

Guillaume Laforge Feb 21

Comparing #Lean and #Rocq (formerly known as Coq)

I thought both were theorem provers, but it seems Rocq is more for building verifiable software, while Lean is for more classical math.

So Lean might be a better fit for the math explorations #LLMs and #AI #Agents are doing for solving problems.

pesco Jan 20

This game (still) rocks.

I binge-completed the first four chapters some time in 2014, did the next four in 2016, and then sadly let the project of finishing "Software Foundations" sit idle for almost ten years. :(

Well, any time is infinitely better than never, so here I go with the significantly expanded 2025 edition!

https://softwarefoundations.cis.upenn.edu/

Image warning: Screenshot spoils the solution to one exercise.

#coq #rocq

José A. Alonso Jan 14

Cylindrical algebraic decomposition in Coq/Rocq. ~ Quentin Vermande. https://dl.acm.org/doi/pdf/10.1145/3779031.3779100 #ITP #Rocq

José A. Alonso Dec 30

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

Readings shared December 29, 2025

The readings shared in Bluesky on 29 December 2025 are: Hint-based SMT proof reconstruction. ~ Joshua Clune, Haniel Barbosa, Jeremy Avigad. #ITP #LeanProver #SMT The biggest controversy in maths coul

Vestigium