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
LSFA 2025 Second Call for Papers
Wed 2025/03/26
Call for papers: FCS @ CSF'25 (Extended deadline: April 6 AoE)
Wed 2025/03/26
Call for Participation, Functional Software Architecture (Oct. 17th, Singapore)
Tue 2025/03/25
Call for Papers, Functional Software Architecture (Deadline June 16)
Tue 2025/03/25
FME Teaching Tutorial on March 28, 2025, 4 pm CET: Prof Peter-Michael Osera, Grinnell College, US, on "Formal Verification and Foundations: Better Together!"
Tue 2025/03/25
ESOP 2026 - Call for Papers
Mon 2025/03/24
ETAPS 2025 - CALL FOR PARTICIPATION
Mon 2025/03/24
Registration reminder for HoTT/UF 2025
Sun 2025/03/23
HCVS 2025 CfP: 12th Workshop on Horn Clauses for Verification and Synthesis, 22 July 2025, Zagreb (Croatia)
Fri 2025/03/21
PhD positions at Stockholm University (deadline April 22)
Wed 2025/03/19
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
#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
Is Coq Interpreted, Compiled, or Executed in a VM?
6 comments
Wed 2024/12/25
