Planet Rocq
Link aggregator of discussions about the
Rocq
interactive theorem prover
Discourse
Constructing the category of categories
9 answers
Sun 2025/04/27
Looking for a Coq Tutor
Sun 2025/04/27
First Rocq'n'share meeting
Fri 2025/04/25
Tenth Mathcomp sharing day
Fri 2025/04/25
[ANN] The Fifth Iris Workshop, June 2-6, 2025, Inria Paris
Tue 2025/04/22
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
Zulip
Funext vs setoids
Rocq as general-purpose language for application development
Sort polymorphism, additional universe variables
Pass list of definitions to an Ltac
Stuck with a proof
Rocq'n'share 2025
✔ Module "Classical" is missing in rocq 9.0
✔ Can't find coqtop in Proof general after upgrade to rocq
New tutorials and how-to
Usability of SProp?
Proof Assistants Stack Exchange
Coq: parametrisable `Variable` or `Context`
1 answer
Sat 2025/04/26
How to formalize Rule 6 meta theorem from Hilbert/Ackermann book
Fri 2025/04/25
Equivalent of `Context` in Lean
2 answers
Fri 2025/04/25
Does functional extensionality imply equality of records wrapping extensionally equal functions in Coq?
3 answers
Fri 2025/04/25
How Do You Use Infeasibility Certificates For Reflection In Intuitionistic Logic
1 answer
Wed 2025/04/23
Coq: how to remove an element from a finType
2 answers
Tue 2025/04/22
Destruction of bound dependent types
2 answers
Mon 2025/04/21
Create a separate module for notations for modules implementing an interface
1 answer
Mon 2025/04/21
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
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
LSFA 2025 Last Call for Papers
Tue 2025/04/22
DaLi 25, 2nd call for papers
Tue 2025/04/22
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
Reddit
Formal protocol demonstrating operative dissociation without altering the classical logical kernel.
Sun 2025/04/27
ChatGPT, draw a picture of mechanized theorem proving
Sun 2025/04/27
When will this sub be renamed?
3 comments
Thu 2025/04/24
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
Stack Overflow
Rocq: Transparent aliased definition (that instance solver sees though)
2 answers
Thu 2025/04/24
How can I rewrite or use my IH when Coq won't unify my goal with it?
1 answer
Mon 2025/04/14
How to prove that it is not possible for a Nil process to take a transition? (Pi-calculus in Coq)
1 answer
Fri 2025/04/04
while_true_nonterm in Lean4
1 answer
Thu 2025/03/20
Is there a way to disable a specific notation in Coq?
3 answers
Tue 2025/03/18
How to apply simple lemma with complex instantiation in Coq?
1 answer
Wed 2025/03/12
How to prove if a list `n::l` is an in-order merge of 2 lists `n::l1` `l2`, then `l` is an in-order merge of `l1` and `l2` in Coq?
1 answer
Mon 2025/03/03
How to reduce a cofix expression?
2 answers
Tue 2025/02/25
Coq vector: shiftin, shiftout, and last
2 answers
Fri 2025/02/14
Coq vector: equality of shiftin
2 answers
Fri 2025/02/14
