Planet Rocq
Link aggregator of discussions about the
Rocq
interactive theorem prover
Discourse
VSTTE 2025: Second call for papers (deadline: July 18th)
Wed 2025/06/18
Postdoc position on type systems for multiple unit systems
Thu 2025/06/12
CFP - JFLA 2026 - Journées Francophones des Langages Applicatifs
Thu 2025/06/12
Branch planning for 9.1
Fri 2025/06/06
How to think of inductive types?
4 answers
Fri 2025/06/06
What is the edit_id or editId in the XML protocol?
1 answer
Fri 2025/06/06
[ANN] coq-lsp 0.2.3
Wed 2025/06/04
Why are tactics like `simpl` valid?
10 answers
Mon 2025/06/02
Autumn school "Proof and Computation", Herrsching (Germany), 14-20 Sep 2025
Thu 2025/05/29
How can I take use of certain Prop when defining a function?
7 answers
Wed 2025/05/28
Zulip
logical foundations - Induction - bin2nat problem
Extensible Parsing Experiments
✔ Typesetting Coq code in Latex
Primitive arrays and nested inductives
All your base are belong to us: 0 level
Should I do a Math or Computer Science Degree?
PLF question: Hoare2 chapter's missing `ap` operator
eqn: makes a basic proof example fail, why?
Where can Rocq be useful to research mathematicians?
Rocq's Trusted Computing Base Is This Big?
Proof Assistants Stack Exchange
Programmatically transform look-up function to a match statement in Rocq
Wed 2025/06/18
How to create an element of sumbool type
2 answers
Tue 2025/06/17
Rocq: "Extra arguments" error while trying to use the "Arguments" command
1 answer
Sun 2025/06/15
Programming language foundations, Equiv: Theorem ptwice_cequiv_pcopy
2 answers
Fri 2025/06/13
Convert a func from nat to A to a stream of A's idiomatically in Rocq
1 answer
Thu 2025/06/12
About the use of command Canonical in Coq for mantaining Record Type information
1 answer
Wed 2025/06/11
Derive a functor (or, fmap) in Rocq automatically
2 answers
Mon 2025/06/09
Is it possible to implement rewrite yourself in Rocq?
2 answers
Sun 2025/06/08
How does `apply term in ident` tactic work in this situation?
2 answers
Sat 2025/06/07
Beginner trying to prove forall A: Prop, (A -> ~A) -> False
1 answer
Sat 2025/06/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
CfP: REACTS'25 - International Workshop on Reconfigurable Transition Systems, Nov 10-11, 2025
Wed 2025/06/18
DataMod 2025 - First Call for Papers
Tue 2025/06/17
Call for faculty positions at PUCV, Chile
Tue 2025/06/17
1st CFP - CPP 2026 - Certified Programs and Proofs
Mon 2025/06/16
Meeting IFIP WG 1.6 on Rewriting: Call for Participation (early registration by *15 June 2025*)
Fri 2025/06/13
Call for participation to UNIF 2025
Thu 2025/06/12
PhD Position in Parametric Floating-Point Reasoning at Uppsala
Wed 2025/06/11
TyDe 2025 - Call for Papers (Submission deadline extended to Jun 22; Remote presentation supported)
Tue 2025/06/10
CADE-30 Call for Participation
Tue 2025/06/10
Assist./Assoc. Professor Positions at NII, Tokyo
Sat 2025/06/07
Reddit
Hints for proving proof rule for Hoare REPEAT command?
1 comment
Thu 2025/06/12
Any good resources on how to add a target for Coq Extraction?
Sun 2025/05/18
When will this sub be renamed?
6 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?
4 comments
Wed 2025/02/19
Stack Overflow
What is the origin of the names of I and tt?
1 answer
Thu 2025/06/12
Providing and using proofs as arguments to a function in Rocq
1 answer
Wed 2025/06/04
Deducing equality from existT equality
2 answers
Mon 2025/05/26
Software Foundations Basics - Theorem lower_grade_lowers need to prove implication Eq = Lt -> Eq = Lt
3 answers
Thu 2025/05/22
How to temporarily disable notations in Coq
2 answers
Fri 2025/05/09
Prove that an element of fin 1 is exactly 0
2 answers
Thu 2025/05/08
Coq: Boolean Comparison of Integers
2 answers
Fri 2025/05/02
In Coq (or Rocq), can't a lemma with a universal conclusion be applied to other premises?
3 answers
Tue 2025/04/29
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
