Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Simple Coq help
6 answers
Thu 2025/01/16
[VsCoq 2] Release 2.2.3
Thu 2025/01/16
Proof-general auto bullet extension
6 answers
Tue 2025/01/07
The Rocq Prover - New identity and website
4 answers
Mon 2025/01/06
How to Efficiently Structure Proofs in Coq for Large Scale Projects?
1 answer
Mon 2025/01/06
Coq be an actual proof assist tool
4 answers
Mon 2025/01/06
Finite sets (MSets) on dependent types
6 answers
Sun 2024/12/22
I compiled the Coq Platform from sources. How do I edit proofs?
4 answers
Sun 2024/12/22
PhD position at Swansea University, UK
Wed 2024/12/18
Use of contradiction tactic
5 answers
Mon 2024/12/16
The Coq Club mailing list
Call for Papers FMBC 2025
Fri 2025/01/17
(Call for Participation) Dafny Workshop at POPL 2025
Fri 2025/01/17
Workshop on Theorem Proving and Machine Learning in the age of LLMs
Thu 2025/01/16
Workshop on Theorem Proving and Machine Learning in the age of LLMs: SoA and Future Perspectives
Wed 2025/01/15
Final CfP for HoTT/UF 2025
Wed 2025/01/15
DisCoTec 2025, 2nd CfP: 20th International Federated Conference on Distributed Computing Techniques
Wed 2025/01/15
Formal Verification of a Safegcd Implementation in C for computing modular inverses
Tue 2025/01/14
Job Ad: Proof Engineer at Cryspen
Tue 2025/01/14
World Logic Day 2025 + GRAPHIC DESIGN CHALLENGE FOR WLD 2026 Happy UNESCO World Logic Day 2025!
Tue 2025/01/14
Offre de thèse sémantique/preuve de programmes à l'ISAE-Supaero et l'ENAC
Mon 2025/01/13
Zulip
How to prove (in)equalities on reals & integers?
opam fails to compile coq-stdlib with ocaml-system 5.2
Flocq should have a NaNs-propagation class
How to insert test condition
✔ combine efect
✔ Pipe character in Instance definition
Coq or Rocq for the upcoming BB(5) paper?
list monad transformer
✔ Top-printers for core tactics
Same notation for relations between multiple types?
Proof Assistants Stack Exchange
Cannot find a physical path bound to logical path on VsCoq when importing a cloned repository
1 answer
Thu 2025/01/16
How to work on Coq with Proof General?
1 answer
Thu 2025/01/16
Can we construct (at least type-check) cyclic terms in Coq?
1 answer
Thu 2025/01/09
How to generate sigma type for a list of letters of a formula
2 answers
Tue 2025/01/07
How to add a formula into context and prove it for assert
1 answer
Mon 2025/01/06
What strategy should I learn to generalize my observations?
1 answer
Sun 2025/01/05
Kalmár proof of completeness theorem
1 answer
Sun 2025/01/05
Why doesn't simpl unfold a pattern-matching in Program Fixpoint with {measure} in Coq?
1 answer
Sun 2025/01/05
Rose tree map function via length-indexed list map function
1 answer
Fri 2025/01/03
Why does `<->` not work here?
1 answer
Thu 2025/01/02
Stack Overflow
Disjunction versus sumbool of exclusive propositions in Coq
1 answer
Wed 2025/01/01
Proving that Multiplication is distributive
1 answer
Tue 2024/12/31
How to destruct evars in Coq?
1 answer
Tue 2024/12/31
How Can I Represent An Assembly Program With Labels?
1 answer
Mon 2024/12/30
How can I prove Proof Irrelevance from Propositional Extensionality in Coq?
3 answers
Sun 2024/12/29
how to prove 2 step induction of list in coq using fix tactic
1 answer
Fri 2024/12/27
Coq Program Fixpoint Obligation Proof
2 answers
Thu 2024/12/26
Theorem for lambda calculus
1 answer
Mon 2024/12/23
What is the difference between Lemma and Theorem in Coq
1 answer
Fri 2024/12/20
Cannot rewrite in goal using Equations Package in Coq?
2 answers
Sat 2024/12/14
CS Theory Stack Exchange
Representations of Planar Graphs in Coq
2 answers
Wed 2025/01/08
Finite sets in Coq
1 answer
Thu 2024/10/03
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
Reddit
Compiling Coq to Imperative Languages Such as C
5 comments
Fri 2025/01/10
Implementing Coq
7 comments
Tue 2025/01/07
I've completely formalized 3 key chapters from Rob's Type Theory and Formal Proof textbook
Sat 2025/01/04
Coq Speed of Execution
2 comments
Wed 2024/12/25
Is Coq Interpreted, Compiled, or Executed in a VM?
4 comments
Wed 2024/12/25
(Coq based) Verified Matching of Regular Expressions with Lookarounds
2 comments
Thu 2024/12/05
Type Theory Forall #46 - Realizability Models, BHK Interpretation, Dialectica - Pierre-Marie Pédrot
Fri 2024/11/29
#45 What is Type Theory and What Properties we Should Care About - Pierre-Marrie Pédrot
Mon 2024/11/25
What are the dangers of using Hilbert's epsilon operator?
2 comments
Fri 2024/09/06
What is a good community for beginner questions?
3 comments
Fri 2024/09/06
