Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Extraction - System error
8 answers
Fri 2021/07/30
Software Foundations: minustwo not found in Poly.v
6 answers
Wed 2021/07/28
Software Foundations: Normalization Function Exercise
2 answers
Mon 2021/07/26
Coq Prove code security
1 answer
Mon 2021/07/26
CoqPL 2022: Call for Presentations
Fri 2021/07/23
Enforcing that the parser and the documented syntax are in sync
Fri 2021/07/16
Defining and working with trivial finite sets like {x, y, z} easily
6 answers
Thu 2021/07/08
Finite types, historical question
2 answers
Wed 2021/07/07
Software foundations: stuck at exercise `binary_inverse` in the Induction chapter
2 answers
Tue 2021/07/06
关于存在变量的提取问题
2 answers
Sun 2021/07/04
The Coq Club mailing list
IJCAR 2022 - Call for Workshops
Fri 2021/07/30
Postdoc at Cornell
Tue 2021/07/27
True arithmetical proposition not provable
45 replies
Tue 2021/07/27
RAMiCS 2021 - Call for short contributions/posters
Mon 2021/07/26
Programmatically generating names for binders
3 replies
Mon 2021/07/26
CICM 2021, July 26-31, Call for online participation
Sun 2021/07/25
Printing proof script after Qed.
7 replies
Sat 2021/07/24
Update: Formalization of Actuarial Mathematics in Coq
Sat 2021/07/24
CoqPL 2022: Call for Presentations
Fri 2021/07/23
Postdoctoral Opening at the University of Minnesota
Thu 2021/07/22
Zulip
Asking for hints to prove a theorem
Rewrite confusion
reading ssreflect related books
Trailing spaces in notation
software foundations coq version?
✔ [Newbie] Problem with clightgen.exe
ANSSI and experimental SProp
Strange newline in printing
✔ interval 4.3.0 plotting failure
snoc induction
Stack Overflow
Can I define an equivalent to this using the Axiom command?
1 answer
Wed 2021/07/28
Coq: proving `P -> ~P -> Q` without `contradiction` tactic?
2 answers
Tue 2021/07/27
Proving two functions are equivalent without exactly the same hypotheses
1 answer
Mon 2021/07/26
How to use a theorem with a match pattern
1 answer
Sat 2021/07/24
Proving an addition function is associative using Coq
2 answers
Fri 2021/07/23
Coq + Emacs? ``Check`` can't see what is defined in the source file
1 answer
Wed 2021/07/21
Coq question. compile errors. [file-no-extension,filesystem] and grammar entry "ident" permitted "_"
1 answer
Wed 2021/07/21
How to avoid true=false condition
1 answer
Sun 2021/07/18
Why does Coquelicot mess with my bullets?
1 answer
Fri 2021/07/16
Coq match on Hypothesis passed to Ltac tactic
1 answer
Wed 2021/07/14
CS Theory Stack Exchange
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
Defining finite sets inductively in a proof assistant?
1 answer
Tue 2020/05/05
Has the compactness theorem for FOL been formalized in Coq/Isabelle/etc?
2 answers
Fri 2020/03/13
Lack of atomic propositions in the Calculus of Constructions from ATTAPL textbook
1 answer
Thu 2020/03/05
Journals or conferences to submit formally verified libraries?
Wed 2020/02/12
Reddit
Type Theory Forall Podcast Episode #10 - Classical Logic vs Intuitionistic Logic, feat. Thorsten Altenkirch and Anupam Das
Wed 2021/07/14
Simple Example of Inductive
5 comments
Tue 2021/06/22
Proving a function body of an Abstract Data Type
3 comments
Mon 2021/05/31
Proving that [insert] produces a Binary Search Tree
5 comments
Sat 2021/05/22
Silveroak - Formal specification and verification of hardware
Thu 2021/05/20
This is My First Non-trivial Coq Development
3 comments
Wed 2021/05/19
Solving a mergesort sorting algorithm in Coq
5 comments
Tue 2021/05/18
Trivial problem with applying lemma.
2 comments
Mon 2021/05/17
How to make a function going from nat to decimal representation?
17 comments
Fri 2021/05/14
Coq-club archives unavailable?
2 comments
Wed 2021/04/21
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
