Planet Rocq

Discourse

• CFP LFMTP26, Logical Frameworks and Meta-Languages: Theory and Practice @FLOC, Lisbon, Portugal, July 24
  Thu 2026/03/26
• Volunteers for ICFP 2026 Artifact Evaluation Committee (AEC)
  Mon 2026/03/23
• CfC: Syntax and Semantics of Type Theories 2026
  Mon 2026/03/23
• MIT Programming Languages Review 2026
  Fri 2026/03/20
• March 23: Proof Assistant WG at ENS de Lyon
  Tue 2026/03/17
• PhD Position in Programming Languages and Program Verification at Aarhus University (Deadline: May 1, 2026)
  Mon 2026/03/16
• Rocq cannot find libraries in Rocq platform
  13 answers
  Mon 2026/03/16
• The first summer school on Programming Languages, Logic, and Software Security
  Fri 2026/03/13
• Iris 4.5 and std++ 1.13 release
  Thu 2026/03/12
• AIPV 2026
  Thu 2026/03/12

Zulip

• Module Signature checking performance
• applying the length function to both sides of an equality
• Rocq Logo
• Transparently splitting up a module into multiple files
• Embedded DSLs with custom Rocq Commands?
• Abstract Binding Trees in Rocq
• ✔ ssreflect rewrite top hypothesis in let definition
• Curiosity about `respectful_hetero`
• ✔ Rewrite not working since Rocq 9
• Equations/funelim does not see inside dependent if construct

Proof Assistants Stack Exchange

• Is it possible to make a "canonical substructure" usable with reversible coercions in Rocq?
  1 answer
  Fri 2026/03/27
• How to debug "Nothing to rewrite" in Rocq?
  Fri 2026/03/27
• Some kind of correspondence between perm_eq and {perm _} in Mathcomp
  2 answers
  Sat 2026/03/21
• Coq - Overloading over multiple parameters with canonical structures
  1 answer
  Mon 2026/03/16
• Inductive vs. recursive definitions
  4 answers
  Wed 2026/03/11
• How hard is this to prove formally (e.g., in Coq)? 3^d1·k - 1 = (2^d1·k - 1)·2^d0 has only solution (1,1,1)
  Tue 2026/03/10
• Coq ssreflect - rewrite inside \big
  1 answer
  Thu 2026/03/05
• Stuck proving the induction hypothesis of multiplication on natural numbers mul_n_S?
  Sat 2026/02/28
• Defining and Instantiating Functors with Partially Defined Members
  1 answer
  Wed 2026/02/25
• Construct the sum of reals indexing on a finType
  1 answer
  Tue 2026/02/24

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

Reddit

• Poule: seeking Claude subscribers to test my Coq LLM tools (MCP, RAG, and more)
  2 comments
  Tue 2026/03/24
• Best practices for Coq validation
  2 comments
  Tue 2026/03/24
• Needed Degree For Learn Coq and Formal Logic?
  8 comments
  Sat 2026/03/14
• Is Chlipala's book Certified Programming with Dependent Types a good start?
  5 comments
  Wed 2026/02/04
• Why do some Stdlib theorems leave open the possibility of negative naturals?
  6 comments
  Mon 2026/01/19
• Ok I don't get this.
  1 comment
  Wed 2026/01/07
• How can i rewrite expressions?
  4 comments
  Mon 2026/01/05
• Rocq doesn't find a word-for-word copy-paste from the goal
  2 comments
  Tue 2025/11/11
• Need help to understand coinductive proofs.
  2 comments
  Fri 2025/10/31
• Has anyone done Certified Programming with Dependent Types recently?
  6 comments
  Wed 2025/10/29

Stack Overflow

• Which vector library to use in coq?
  2 answers
  Sun 2026/03/22
• Can we prove equal subcases have equal induction hypotheses in recursion principle?
  6 answers
  Tue 2026/02/24
• 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
• How can one handle by case analysis a boolP expression in Coq/ssreflect?
  2 answers
  Wed 2025/09/10
• How can one handle dependent-type equality proofs (sigma types) in Coq?
  2 answers
  Tue 2025/09/09