Planet Coq

Link aggregator of discussions about the Coq interactive theorem prover

Discourse

Contradicting instructions for installation with OPAM
2 answers
Tue 2021/03/02
Extraction to Haskell Int type
1 answer
Mon 2021/03/01
Release of the Coq platform 2021.02.0
Fri 2021/02/26
What axioms are built-in?
5 answers
Thu 2021/02/25
Release of Coq 8.13.1
Tue 2021/02/23
Hydra battles
Mon 2021/02/22
[CFP] The Coq Workshop 2021 : Call for Talk Proposals
Wed 2021/02/17
Add LoadPath in Coq 8.12.2
2 answers
Fri 2021/02/12
Application of automatic induction principle versus induction tactic
2 answers
Sun 2021/02/07
Inversion of an axiom is bad
6 answers
Sat 2021/02/06

The Coq Club mailing list

[CFP] AFADL 2021
Tue 2021/03/02
ETAPS 2021 call for participation
Mon 2021/03/01
19 replies
Mon 2021/03/01
Release of the Coq platform 2021.02.0
Fri 2021/02/26
ACKERMANN AWARD 2021: CALL FOR NOMINATIONS
Fri 2021/02/26
Postdoc/phd positions in ERC project "Certified Quantum Security" (formal verification of quantum crypto)
Thu 2021/02/25
Searching for a remote part-time position
Thu 2021/02/25
Zarith - compiling Coq 8.13 on Debian stable
3 replies
Thu 2021/02/25
Research Internships using Coq at CertiK
Wed 2021/02/24
F-IDE 2021 - Last Call for Papers - Extended Deadline
Wed 2021/02/24

Zulip

Stack Overflow

VST built-in annotation support
Tue 2021/03/02
Theorem + induction vs Fixpoint + destruct in Coq
1 answer
Tue 2021/03/02
Proving coinductive theorems with coinductive assumptions
1 answer
Sun 2021/02/28
How to constrain a type field to a power of two in a type system?
1 answer
Sat 2021/02/27
How to implement a spec and prove it using kami?
Tue 2021/02/23
Translating proof from Nat to Rat
1 answer
Sun 2021/02/21
How to prove for all functions P, Q from typical type to `Prop`, "forall a, b, P(a) or Q(b) holds" iff "forall a, P(a), or, forall b, Q(b), holds"?
1 answer
Sat 2021/02/20
Compiling multiple Coq files does not work
1 answer
Thu 2021/02/18
Puzzle of induction in Coq
Wed 2021/02/17
Defining integers inductively in Coq (inductive definitions subject to relations)
1 answer
Tue 2021/02/16

CS Theory Stack Exchange

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
1 answer
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
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

Reddit

The Type Theory Forall Podcast #5 - The History of Coq'Art (Yves Bertot)
1 comment
Sun 2021/02/28
A formal proof of safegcd bounds
Sun 2021/02/21
Simple untyped lambda calculus interpreter
1 comment
Sat 2021/02/13
Is there some sort of archive of formal proofs for Coq?
2 comments
Wed 2021/02/10
Approach for Packet Manipulation when extracting to OCaml?
Sun 2021/02/07
Memoization
4 comments
Fri 2021/01/08
Why is the grammar for Coq extensible and not fixed?
3 comments
Thu 2021/01/07
Other languages?
7 comments
Mon 2020/12/28
The Entire Evolution of Coq (source code visualization)
Sun 2020/12/27
Beginner help writing a recursive square root finding function in Coq
2 comments
Sat 2020/12/26

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