Planet Coq

Link aggregator of discussions about the Coq interactive theorem prover

Discourse

Bug in universe inference?
Mon 2020/10/26
Stuck at Multiset.v contents_cons_inv
1 answer
Sun 2020/10/25
Ad hoc asynchronicity
10 answers
Fri 2020/10/23
Next CUDW 2020/11/30 to 2020/12/04 — Save the Date!
1 answer
Thu 2020/10/22
Why induction principle such as list_rect cannot be added in Hint database?
2 answers
Wed 2020/10/21
Trying to prove sort algorithm correctness (for specific n), in search for hints
11 answers
Tue 2020/10/20
Tree Calculus
Wed 2020/10/14
Announcing Coq 8.12 support for Codewars
1 answer
Wed 2020/10/14
Inserting PPX annotations into extracted OCaml
2 answers
Mon 2020/10/12
Pattern matching: warn unused parameter?
1 answer
Sat 2020/10/10

The Coq Club mailing list

Faculty position at Portland State University
Sun 2020/10/25
Need help making a modular reflection reifier
3 replies
Fri 2020/10/23
ICALP 2021 Call for Workshops
Wed 2020/10/21
CADE-28: Call for Papers, Workshops, Tutorials and Competitions
Wed 2020/10/21
CADE-28 Call for Papers, Workshops, Tutorials, Competitions
Tue 2020/10/20
ITP 2021: Call for Papers
Tue 2020/10/20
Research position in Formal Verification (m/f/x) at HENSOLDT Cyber in Munich
Tue 2020/10/20
LICS 2021 Call for Papers
Mon 2020/10/19
F-IDE 2021 - Call for Papers
Mon 2020/10/19
LICS 2021 Call for Workshops
Mon 2020/10/19

Zulip

Stack Overflow

Equality on complex functions with complex type
2 answers
Sun 2020/10/25
Automatically proving a non-linear arithmetic proposition over Z in Coq
Sat 2020/10/24
Equality on complex functions
1 answer
Fri 2020/10/23
Is there a good strategy for proving the given teorem?
1 answer
Thu 2020/10/22
How to prove equivalence between those two types - algorithm' and algorithm''?
1 answer
Mon 2020/10/19
Z_3: left inversion lemma
1 answer
Sun 2020/10/18
Coq unable to unify -- how to change hypothesis?
1 answer
Sat 2020/10/17
How to apply a constructor in an hypothesis?
1 answer
Sat 2020/10/17
Messing around with category theory
1 answer
Fri 2020/10/16
Z_3: left id proof
1 answer
Fri 2020/10/16

CS Theory Stack Exchange

An axiom for John Major's Equality
1 answer
Sun 2020/09/20
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
On the interpretation of coinduction in type theory
Mon 2019/12/23
Have the proofs in Buss's "On Goedel’s Theorems on Lengths of Proofs" been formalized (mechanically checked)?
Fri 2019/12/13
Proposition terms vs types in Coq
Mon 2019/12/02
Prove proof irrelevance in Coq?
1 answer
Mon 2019/08/26
Model of Coq (pCuIC) in higher toposes?
Tue 2019/08/13

Reddit

Is it normal to complete a proof without really knowing what's going on?
7 comments
Sat 2020/10/17
Understanding destruct
2 comments
Wed 2020/10/14
ANSSI released reviewing standards for Coq proofs placing Coq at the highest (EAL7) level for software verification
1 comment
Wed 2020/09/23
Interfacing with Coq
2 comments
Wed 2020/09/23
A Series on Ltac
2 comments
Thu 2020/09/17
Proving things about bool functions
4 comments
Tue 2020/09/15
Some proofs about sequences and series
1 comment
Sun 2020/09/13
New Software Foundations volume: "Verifiable C" by Appel and Cao
8 comments
Sat 2020/09/12
Program Logics for Certified Compilers
1 comment
Tue 2020/09/08
Installation -- HELP!
12 comments
Fri 2020/08/21

Coq News

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
Coq 8.11.0 is out
Tue 2020/01/28
Coq 8.11+beta1 is out
Fri 2019/12/06
Coq 8.10.2 is out
Fri 2019/11/29
Coq 8.10.1 is out
Fri 2019/10/25
Coq 8.10.0 is out
Mon 2019/10/07
Coq 8.10+beta3 is out
Mon 2019/09/16