Planet Rocq
Link aggregator of discussions about the
Rocq
interactive theorem prover
Discourse
TYPES 2026: Post-proceedings Call for Papers
Wed 2026/09/23
Postdoc position at TU Delft
Wed 2026/09/16
NWPT 2026, Final Call for Contributions
Tue 2026/09/15
RocqPL 2027 Call for Presentations
Wed 2026/09/09
JFLA 2027: Second Appel à Communications
Tue 2026/09/08
Chaire de Professeur Junior in Lyon: Generative AI for formal proofs
Thu 2026/08/27
ANU International Logic Summer School, 7–18 December
Sun 2026/08/23
Call for Nominations: POPL 2027 Artificat Evaluation Committee
Tue 2026/08/18
Mathcomp 2.6.0 released
Tue 2026/08/18
We are paying math researchers to capture the work you are already doing!
Mon 2026/08/17
Zulip
Status of SProp
Under the hood of Search
syntax for abstract tactic block
Ocaml recommended version
Implicits in class constraints
Rocq termination checking
Complexity Theory
Recursively defined theorem with some measure
Notation prints differently when integers are involved
AI agents for writing proofs
Proof Assistants Stack Exchange
Is `rat` harder to use than `Q` for rational numbers in Rocq?
1 answer
Tue 2026/09/22
Debug autorewrite in Coq
1 answer
Fri 2026/09/11
Make [...] explicit in Rocq/vsRocq
1 answer
Wed 2026/09/02
Non-typed dependent pattern matching in Rocq
1 answer
Thu 2026/08/20
An upgrade from Mathcomp v2.4.0 to v2.5.0 going wrong with rationals
1 answer
Sat 2026/08/15
Error when making CoqProject
2 answers
Mon 2026/08/03
Is there a model that contradicts `@eq Type t1 t2 -> @eq Prop t1 t2` or can it be proven?
1 answer
Sun 2026/08/02
Induction COQ Question
2 answers
Sun 2026/08/02
How to prove commutation of a recursive function over a finite set encoded with binary nat in coq
1 answer
Fri 2026/07/31
Declaring builders with Hierarchy Builder (Rocq)
1 answer
Thu 2026/07/16
CS Theory Stack Exchange
Coq proof - no verifier can be simultaneously sound and complete on a µ-sensitive claim from an identical classical trace. Check me please!
Thu 2026/09/10
Is injectivity of constructors for (large) inductive types in Prop, such as squashing, consistent?
Mon 2026/04/27
Finite sets in Coq
1 answer
Fri 2025/01/31
Representations of Planar Graphs in Coq
2 answers
Wed 2025/01/08
Simple Coq simplification question
1 answer
Fri 2024/06/07
What should a proof of correctness for a typechecker actually be proving?
3 answers
Thu 2024/06/06
Formalization of matching logic (logic behind K Framework)
3 answers
Wed 2023/08/16
Notation problem
1 answer
Thu 2023/06/01
Can I define nested mutually dependent types in Coq?
1 answer
Sat 2023/05/13
Defining finite sets inductively in a proof assistant?
1 answer
Tue 2023/04/25
Stack Overflow
Trouble with well-foundedness proofs
Sat 2026/07/11
How to get the fully qualified name of a Rocq tactic?
2 answers
Wed 2026/06/24
Is it possible to convert all higher-order logic and dependent type in Lean/Isabelle/Coq into first-order logic?
1 answer
Wed 2026/05/20
Which vector library to use in coq?
2 answers
Sun 2026/03/22
Coq (Rocq) standard library function for converting nat to string?
1 answer
Wed 2026/02/11
Equality of type with equal indices do not typecheck
3 answers
Wed 2026/01/28
How to prove manually (using calc) a Dafny lemma with an existential variable?
3 answers
Sun 2026/01/25
Kind of issue with two-steps recursion
2 answers
Fri 2026/01/09
How to scrutinize a `match` term with return type `a=b -> c`
1 answer
Mon 2025/10/20
How to deal with potentially-aliased arguments in VST?
1 answer
Sat 2025/09/13
