Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Is there a way to prove properties about ocaml programs using a Coq verified library
2 answers
Sun 2021/01/24
Can I extract part of a module instead of the whole module?
Wed 2021/01/20
Cite Coq Library Materials
Sat 2021/01/16
Force application of fixpoint to its argument
11 answers
Fri 2021/01/15
What is the difference between Gallina and Ltac?
6 answers
Fri 2021/01/15
avoiding type error
10 answers
Thu 2021/01/14
A formal proof of Abel-Ruffini Theorem in Coq
Wed 2021/01/13
Release of Coq 8.13.0
Tue 2021/01/12
Program equivalence and substitution
3 answers
Fri 2021/01/08
Soundness of program transformation
2 answers
Thu 2021/01/07
The Coq Club mailing list
meaning of formal specifications
10 replies
Tue 2021/01/26
installing coq using opam
2 replies
Sat 2021/01/23
solving Qc inequalities
2 replies
Fri 2021/01/22
[Lambda Days + TFP + TFPIE 2021] call for participation
Fri 2021/01/22
OCaml extraction and proof obligations
3 replies
Fri 2021/01/22
CfP - Intersection Types and Related Systems - ITRS2021
Fri 2021/01/22
Two fully funded PhD positions in type theory at Chalmers/Gothenburg Univ
Thu 2021/01/21
A fast "eq" predicate for Gallina?
14 replies
Thu 2021/01/21
Add LoadPath in Coq 8.12.2
11 replies
Wed 2021/01/20
ill-typed evar instantiated (caught later at Qed)
Tue 2021/01/19
Zulip
`Let` produces beta-redexes
Finding notations
Beginner : iterator on a context in Ltac
Backtracking TC search & `Hint Extern`
From Docker with love
Induction scheme for a range of Z
`cbv`,`Set Debug Cbv`, and `Hint Transparent`
How to check the source code of CompCert
let in with pair in Latc (beginner)
Notation levels for abbreviation
Stack Overflow
How does one display an arbitrary programming language (e.g. Isabelle/Isar) in latex in their native display in *.pdf format?
Tue 2021/01/26
Coq module "Cannot find a physical path bound to logical path matching suffix <> and prefix" and "not found in the loadpath"
1 answer
Mon 2021/01/25
Theorem that finding in a list works properly
2 answers
Sun 2021/01/24
Can I stack implicit types somehow?
1 answer
Wed 2021/01/20
How is an infinite type hierarchy implemented?
Wed 2021/01/20
Distributing subtraction over bigop
3 answers
Tue 2021/01/19
Type coercion from nat to rat
2 answers
Tue 2021/01/19
How can we define `eqType` for dependent types?
2 answers
Mon 2021/01/18
SSreflect not working with Emacs, Coq and ProofGeneral. How to install SSreflect in MacOS?
1 answer
Mon 2021/01/18
string comparison in ssreflect
1 answer
Mon 2021/01/18
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
Memoization
2 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
How to use Z.div_mod, which produces a "let in..." ?
5 comments
Wed 2020/12/23
An experience report on writing usable DSLs in Coq (extended abstract, pdf)
Fri 2020/12/18
A Setter for Length Indexed Lists
8 comments
Thu 2020/12/17
Type checking of types parameterized by nats
2 comments
Tue 2020/12/15
Stuck with a definition for an Imp program
8 comments
Thu 2020/12/10
Coq News
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
Coq 8.11.0 is out
Tue 2020/01/28
Coq 8.11+beta1 is out
Fri 2019/12/06
