Planet Rocq
Link aggregator of discussions about the
Rocq
interactive theorem prover
Discourse
How to formalize dependent setoid morphisms?
4 answers
Tue 2025/07/08
Rocqshop 2025 call for presentations
1 answer
Tue 2025/07/08
Release of Iris 4.4 and std++ 1.12, Announcement of iris-contrib
Wed 2025/07/02
Non-constructive proof
19 answers
Mon 2025/06/30
Announcement: opam-repository (opam.ocaml.org) archiving process
Tue 2025/06/24
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
What is the edit_id or editId in the XML protocol?
1 answer
Fri 2025/06/06
Zulip
Install Ubuntu 24.04 fails ; dune.configurator, elpi
Resources for learning about Extraction (to OCaml)
Problem in a function to destructure a reflection ??
Forcing Qed to use the same reduction strategy as in proof
Apply quantified exists in hypotheses
✔ How to build and import a Coq package into jscoq
non- VS maximally inserted implicit arguments
Why does Rocq overflow?
Intuitionistic drinker
How do I code this (simple?) coercion?
Proof Assistants Stack Exchange
Dune version error while installing the Coq platform
1 answer
Fri 2025/07/11
How did I get this goal by inducting over Permutation?
2 answers
Thu 2025/07/10
Mathcomp import not working
Tue 2025/07/08
Prove x mod x = 0
1 answer
Fri 2025/07/04
GCd definition: cannot guess decreasing argument of fix
3 answers
Tue 2025/07/01
Defining and Instantiating Functors with Partially Defined Members
1 answer
Mon 2025/06/30
Is there a way to rename parameters when including/reusing a module type in Coq?
1 answer
Sun 2025/06/29
Calculus of (inductive) Constructions: Do inductive definitions increase proof strength?
3 answers
Sat 2025/06/28
Proving that a type does not belong to a type class
1 answer
Thu 2025/06/26
How to create a notation for a function in a type class parameter
1 answer
Thu 2025/06/26
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
Temporary software engineer position at Inria, ENS Lyon
Fri 2025/07/11
FSCD 2025: Free online participation, 15 - 18 July 2025
Wed 2025/07/09
OCAML'25: Extended Deadline for The OCaml Users and Developers Workshop
Tue 2025/07/08
[SUBMISSION LINK ADDED] Rocqshop 2025 call for presentations
Tue 2025/07/08
Postdoc positions in type theory, closing date: 25 July
Mon 2025/07/07
CSL 2026 - Second Call for Papers
Sat 2025/07/05
Call for Submissions: SPLASH Doctoral Symposium 2025
Wed 2025/07/02
Rocqshop 2025 call for presentations
Wed 2025/07/02
Release of Iris 4.4 and std++ 1.12, Announcement of iris-contrib
Wed 2025/07/02
Postdoctoral Researcher Position at the University of Tartu
Tue 2025/07/01
Reddit
Why is it permittable to pass Prop where Set is expected?
1 comment
Sun 2025/07/06
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
Stack Overflow
How to understand `(elimTF andP top)`?
1 answer
Fri 2025/06/27
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
