Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Failing to prove that substituting "by hand" is equivalent to... well, substituting
2 answers
Sat 2021/11/13
Preview of Ltac Visual Debugger in CoqIDE is now available
Mon 2021/11/08
Coq Platform 2021.09.0
Mon 2021/11/08
Iris 3.5 and std++ 1.6 released
Mon 2021/11/08
Existentially quantified coinductive predicates
2 answers
Fri 2021/11/05
'rewrite' doesn't want to match large expression
1 answer
Tue 2021/11/02
Tvals in my code is the total map, why coq insists it is not?
3 answers
Tue 2021/11/02
Turing: a library to teach Introduction to the Theory of Computation (Fall'21)
2 answers
Mon 2021/11/01
MathComp 1.13.0 released
Thu 2021/10/28
Thinking of using hammer/automation to guide the order of proving lemmas
Sun 2021/10/24
The Coq Club mailing list
16 Bit Unsigned Integer Library
3 replies
Fri 2021/12/03
10 PhD studentships in Nottingham
Thu 2021/12/02
A style guide for Coq
7 replies
Thu 2021/12/02
Trends in Functional Programming in Education 2022 2nd call for submissions
Thu 2021/12/02
Full-time position in formal verification
Tue 2021/11/30
iFM 2022 (Integrated Formal Methods): Call for Papers
Mon 2021/11/29
A well-order on lists of natural numbers
12 replies
Mon 2021/11/29
Book Publication: Formal Semantics in Modern Type Theories (S. Chatzikyriakidis and Z. Luo)
Thu 2021/11/25
extract logical path name of a .vo file
2 replies
Tue 2021/11/23
MSFP 2022 - First Call for Papers
Mon 2021/11/22
Zulip
Using one recursive notation from another?
List formation
'Extraction' to a different language
list length
how termination is proved in Coq?
✔ turn off coercions
Int63 fold
Using Gallina in formal mathematics
Hint priority in typeclasses eauto with multiple DBs
Disadvantages to HoTT?
Stack Overflow
Proof with multiple cases theorem
2 answers
Fri 2021/12/03
Difference between parameters and members of a class
2 answers
Fri 2021/12/03
How to proove that all elements in a list are smaller than a given element in coq
2 answers
Thu 2021/12/02
How can I proove 0 <= a < b -> rem a b = a in Coq?
1 answer
Thu 2021/12/02
Proving existance by providing an example
1 answer
Thu 2021/12/02
Coq/SSReflect: standard way to case on (x < y) + (x == y) + (y < x)?
1 answer
Wed 2021/12/01
Unable to split a conjunction in Hypothesis
1 answer
Mon 2021/11/29
Select_perm' lemma
1 answer
Mon 2021/11/29
Solving a split proof in Coq
1 answer
Mon 2021/11/29
Coq: a vicious circle with two identical subgoals
2 answers
Mon 2021/11/29
CS Theory Stack Exchange
Prove proof irrelevance in Coq?
1 answer
Fri 2021/10/29
How does axiom K contradict univalence?
2 answers
Sun 2021/09/26
Does the order of declarations in an inductive type matter?
3 answers
Sat 2021/09/25
How would I go about learning the underlying theory of the Coq proof assistant?
4 answers
Wed 2021/08/18
Why does Coq have Prop?
4 answers
Fri 2021/04/09
Dependent eliminator for empty type in intensional Martin-Löf type theory
1 answer
Sun 2021/03/28
Defining inductive types in intensional type theory purely in terms of type-theoretic data
1 answer
Fri 2021/03/19
Impredicativity + large eliminations (with no excluded middle) in Coq
1 answer
Thu 2021/03/04
What do we call a type system where any term of any type ultimately parses down to $*:\mathbf{1}$?
Sat 2021/01/23
An axiom for John Major's Equality
Tue 2021/01/19
Reddit
Help the Proof Assistants Stack Exchange reach Beta!
1 comment
Sun 2021/11/21
The proposal for a proof assistants StackExchange site
Sat 2021/11/20
On proving lists infinite
Tue 2021/10/26
A Verified Online Monitor for Metric Temporal Logic with Quantitative Semantics
3 comments
Fri 2021/10/01
Formal verification manager job at Google - Coq experience a plus
1 comment
Thu 2021/09/23
New to Coq: How to compile .vo files and run command line?
2 comments
Sun 2021/09/05
Slides & Videos of the Coq Workshop 2021
Mon 2021/08/30
Is Coq’ Art book still worth it?
6 comments
Wed 2021/08/11
Clashing versions of ocaml on cpdt text compile
4 comments
Tue 2021/08/10
Join together types
2 comments
Fri 2021/08/06
Coq News
Coq Platform 2021.02.0 is out
Fri 2021/02/26
Coq 8.13.1 is out
Mon 2021/02/22
Coq 8.13.0 is out
Thu 2021/01/07
Coq 8.12.2 is out
Fri 2020/12/11
Coq 8.13+beta1 is out
Mon 2020/12/07
Coq 8.12.1 is out
Mon 2020/11/16
Coq 8.12.0 is out
Mon 2020/07/27
Coq 8.12+beta1 is out
Wed 2020/06/17
Coq 8.11.2 is out
Tue 2020/06/09
Coq 8.11.1 is out
Fri 2020/04/24
