Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Rocq 9.0+rc1 has just been tagged
2 answers
Thu 2025/02/13
Figuring out How Rocq Imports Affect the names available to Smartlocate.global_alias_* calls in an OCaml Plugin
2 answers
Wed 2025/02/12
Learning SSReflect by messing around with primes
3 answers
Mon 2025/02/03
Equations 1.3.1 for Rocq 9.0
Wed 2025/01/29
Coq 8.20.1 is out
Mon 2025/01/20
The Rocq Prover - New identity and website
5 answers
Sat 2025/01/18
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
How to Efficiently Structure Proofs in Coq for Large Scale Projects?
1 answer
Mon 2025/01/06
The Coq Club mailing list
CFP: RSSRail 2025: 6th International Conference on Reliability, Safety, and Security of Railway Systems
Thu 2025/02/13
FSCD 2025: Extended deadline (Abstract: February 17/ Submission: February 22)
Wed 2025/02/12
Scottish Programming Languages and Verification Summer School 2025 at the University of Edinburgh
Tue 2025/02/11
2nd CfC: Proof Assistants Special Session @ North American ASL Meeting (May 15 & 16, 2025, Las Cruces, NM)
Tue 2025/02/11
Fully-funded PhD position in Static Analysis at Inria Lille, France
Tue 2025/02/11
rename bound variable
1 reply
Mon 2025/02/10
TYPES 2025: Second Call for Contributions
Mon 2025/02/10
Fully funded PhD position at KU Leuven on Mechanized Systems-Level Security (Deadline 2025-03-16)
Fri 2025/02/07
Paid internship position at Virginia Tech, USA
Thu 2025/02/06
[CFP] 1st Int. Conf. on Quantum Software :: Submission Deadline - 18th February
1 reply
Wed 2025/02/05
Zulip
Proofs with a set hypothesis
List all identifiers defined in Coq files
(Co)inductive types and fixed points
✔ Ltac: Difference progress and success
Ltac: par:
Spurious "pat" variable in fun '... => … construct
gcd value
ProperProxy and rewrite constraints
Using `Reserved Infix`
Proving Inversion of Fin.t
Proof Assistants Stack Exchange
Coq: a tactic for propositional calculus + equality
1 answer
Thu 2025/02/13
Exploring the Use of Coq in Teaching Proofs – Looking for Similar Researchs
3 answers
Thu 2025/02/13
Coq; Define a function functional_choice
1 answer
Wed 2025/02/12
About the use of command Canonical in Coq for mantaining Record Type information
1 answer
Tue 2025/02/11
Data structure for statement letters values in Kalmár proof of completeness
1 answer
Tue 2025/02/11
Proving pair of paths give a path in Sigma type in HoTT
2 answers
Sat 2025/02/08
Is there idiom bracket or `liftA2` in Coq?
1 answer
Sat 2025/02/08
How to extract the equality between the second projection in an existential in Coq?
2 answers
Fri 2025/02/07
Making a "vector" out of a list violates strict positivity in Coq
1 answer
Wed 2025/02/05
How to write down the product type between two `nat` in Coq?
1 answer
Wed 2025/02/05
Stack Overflow
Coq vector: equality of shiftin
3 answers
Fri 2025/02/14
Coq vector: shiftin, shiftout, and last
Fri 2025/02/14
How can I prove the following in Coq
3 answers
Wed 2025/02/12
Rocq: Transparent aliased definition (that instance solver sees though)
2 answers
Sun 2025/02/09
Proving (p->q)->(~q->~p) using Coq Proof Assistant
4 answers
Fri 2025/01/31
why can't i weaken my goal in coq? (beginner)
Thu 2025/01/30
Why are logical connectives and booleans separate in Coq?
1 answer
Wed 2025/01/29
What's the difference between Program Fixpoint and Function in Coq?
1 answer
Tue 2025/01/21
Is there any difference between "parameters" and "indices" in Coq theorems?
2 answers
Mon 2025/01/20
Disjunction versus sumbool of exclusive propositions in Coq
1 answer
Wed 2025/01/01
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
Reddit
Isabelle student getting to know with Coq
2 comments
Thu 2025/01/30
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?
6 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
