Planet Rocq
Link aggregator of discussions about the
Rocq
interactive theorem prover
Discourse
MathComp 2.4.0 released
Mon 2025/04/14
Coq Platform release with Coq 8.20
Mon 2025/04/14
Can you do IO in Rocq?
4 answers
Sun 2025/04/13
Internships in software verification
Mon 2025/04/07
Looking for testers for ProofGeneral + coq9 (+ rocq cli)
Thu 2025/04/03
Basic questions on polymorphic universes
2 answers
Tue 2025/04/01
Rocq Platform Docs: announcement and call to contribution
Wed 2025/03/26
MetaRocq 1.4 for Rocq 9.0
Wed 2025/03/26
Ninth Mathcomp sharing day
Mon 2025/03/24
How to implement setoid_rewrite for "partial equivalence-relation" in Coq?
1 answer
Fri 2025/03/14
Zulip
Extraction: different behavior on syntactically equal terms
Reflection and the TCB
What is the difference between `intuition` and `firstorder`?
Rocq as general-purpose language for application development
Debugging canonical structures failure
✔ coqc: Using a compiled file in current directory
Generalizable Variable S
✔ docker-coq-action
where can i find the definition for boolean algebra
Induction principle help
Proof Assistants Stack Exchange
Coq: create custom tactic for repeated actions
1 answer
Thu 2025/04/17
Programming language foundations, Types: step_deterministic
1 answer
Wed 2025/04/16
Coq: well founded order on Mathcomp's finTypes
1 answer
Tue 2025/04/15
Coq: prove existence of members based on cardinal
1 answer
Sun 2025/04/13
confused about stlc from Programming Language Foundations
1 answer
Sat 2025/04/12
Rewriting with heterogeneous equality (JMeq)
1 answer
Thu 2025/04/10
Error when making CoqProject
2 answers
Thu 2025/04/10
Software foundations STLCArith: nvalue type definition and progress theorem
1 answer
Thu 2025/04/10
Induction COQ Question
2 answers
Wed 2025/04/09
Why does my custom John Major's equality fail where the standard one works?
1 answer
Mon 2025/04/07
CS Theory Stack Exchange
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
Yet another constructive (Coq) proof that `nat -> nat -> nat` is not bijective. How to explain it to myself?
3 answers
Thu 2023/03/23
Why does Coq have Prop?
4 answers
Fri 2022/12/09
The Coq Club mailing list
DisCoTec 2025 Call for Participation
Thu 2025/04/17
ACL2-2025 Second Call for Participation
Mon 2025/04/14
Coq Platform release with Coq 8.20
Mon 2025/04/14
Ackermann Award: First call for nominations - Deadline 1st July
Mon 2025/04/14
TyDe 2025 - call for papers & extended abstracts
Fri 2025/04/11
Call for Papers: 23rd International Workshop on Satisfiability Modulo Theories
Wed 2025/04/09
CICM 2025: 3rd Announcement and Call for Papers
Wed 2025/04/09
French Spring School in Theoretical Computer Science EPIT 2025 --- last days before registration deadline
Tue 2025/04/08
UNIF 2025 2nd Call for Papers
Mon 2025/04/07
VSTTE 2025: First call for papers
Sun 2025/04/06
Reddit
The statistics of the first 3 volumes of Software Foundations: lines of code & number of exercises
3 comments
Sun 2025/04/06
Need help with proving a Theorem.
6 comments
Sat 2025/03/29
Scottish Programming Languages and Verification Summer School 2025
Fri 2025/03/28
#49 Self-Education in PL - Ryan Brewer
1 comment
Sat 2025/03/15
If you don't understand Fixpoint and Inductive Types, I've created a programming language to help you
2 comments
Thu 2025/03/13
Proving type preservation with STLC
5 comments
Wed 2025/02/26
What happened to renaming Coq?
3 comments
Wed 2025/02/19
Isabelle student getting to know with Coq
2 comments
Thu 2025/01/30
Compiling Coq to Imperative Languages Such as C
5 comments
Fri 2025/01/10
Implementing Coq
8 comments
Tue 2025/01/07
Stack Overflow
Rocq: Transparent aliased definition (that instance solver sees though)
2 answers
Thu 2025/03/13
