Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
How to implement setoid_rewrite for "partial equivalence-relation" in Coq?
1 answer
Fri 2025/03/14
A Short Survey on Type-Driven Development Tools
Fri 2025/03/14
Fully funded PhD position at KU Leuven on Mechanized Systems-Level Security (Deadline 2025-03-16)
Mon 2025/03/03
Docker image of the Rocq Prover (rocq/rocq-prover:9.0)
Mon 2025/03/03
Refinedc install: make under opam can't find dune
1 answer
Sat 2025/03/01
[VsCoq] Release 2.2.5
Thu 2025/02/27
Mini-symposium on proof assistants for education
Thu 2025/02/27
[VsCoq] Release 2.2.4
Thu 2025/02/20
Figuring out How Rocq Imports Affect the names available to Smartlocate.global_alias_* calls in an OCaml Plugin
3 answers
Fri 2025/02/14
Learning SSReflect by messing around with primes
3 answers
Mon 2025/02/03
The Coq Club mailing list
Professorhip in » Logic and Verification in Computer Science «
Fri 2025/03/28
Deadline extension (9 April): GPCE 2025
Fri 2025/03/28
FINAL CFP: CONCUR 2025
Fri 2025/03/28
[ANN] The Fifth Iris Workshop, June 2-6, 2025, Inria Paris
Fri 2025/03/28
Haskell Symposium 2025 First Call for Papers
Thu 2025/03/27
Call for Papers - The 28th Forum on specification and Design Languages (FDL)
Thu 2025/03/27
Call for Nominations: SLE 2025 - Artifact Evaluation Committee, Nominations Wanted
Thu 2025/03/27
LFMTP 2025, First Call for Papers - Birmingham, UK
Wed 2025/03/26
LSFA 2025 Second Call for Papers
Wed 2025/03/26
Rocq Platform Docs: announcement and call to contribution
Wed 2025/03/26
Zulip
Unable to unify ?i2 with ?i2
Online documentation broken?
tauto dual tactic for finding Kripke countermodel
Tauto and Wajsberg/Ben-Yelles algorithm
When are we going to migrate to rocq.zulipchat.com?
✔ Notation ignores implicitness
Lia does not unfold def before solving, normal ?
Tactic Notation "by"
Surveying Automatic BV Solvers - Recs to read / skip?
Reversible coercions, unification looping
Proof Assistants Stack Exchange
How is calculus of constructions implemented in proof assistants?
2 answers
Tue 2025/03/25
Coq - Overloading over multiple parameters with canonical structures
1 answer
Fri 2025/03/21
Coq: link `==` to `=`
2 answers
Wed 2025/03/19
Software foundation: substi_correct excersize
3 answers
Wed 2025/03/19
Formalizing that formula is a tautology
1 answer
Mon 2025/03/17
pCIC vs indexed inductive-recursive definitions and more
1 answer
Sat 2025/03/15
How can I see the version of a library installed with Rocq platform?
1 answer
Fri 2025/03/14
How can I install a Rocq library without opam?
1 answer
Fri 2025/03/14
How to construct a multiset of Coq.Sets.Multiset
2 answers
Fri 2025/03/14
Proving correctness of boolean equality function for untyped lambda calculus terms
1 answer
Thu 2025/03/13
Stack Overflow
while_true_nonterm in Lean4
1 answer
Thu 2025/03/20
Is there a way to disable a specific notation in Coq?
3 answers
Tue 2025/03/18
Rocq: Transparent aliased definition (that instance solver sees though)
2 answers
Thu 2025/03/13
How to apply simple lemma with complex instantiation in Coq?
1 answer
Wed 2025/03/12
How to prove if a list `n::l` is an in-order merge of 2 lists `n::l1` `l2`, then `l` is an in-order merge of `l1` and `l2` in Coq?
1 answer
Mon 2025/03/03
How to reduce a cofix expression?
2 answers
Tue 2025/02/25
Coq vector: shiftin, shiftout, and last
2 answers
Fri 2025/02/14
Coq vector: equality of shiftin
2 answers
Fri 2025/02/14
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
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
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?
3 comments
Wed 2025/02/19
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
