Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
CompCert receives ACM Software System Award
Wed 2022/05/11
Coq Working Group June 2022
4 answers
Wed 2022/05/11
HTT 1.0 released
Wed 2022/05/04
HoTTEST Summer School July+August 2022
Sat 2022/04/30
Using Add Relation for Setoid equivalence of rationals
Tue 2022/04/26
One weird trick to encode modal types
Mon 2022/04/25
Calling Coq from OCaml
1 answer
Fri 2022/04/22
Coq Platform release 2022.04.0
Thu 2022/04/21
How to import Basics.v in Induction.v of LF using VS Coq extension
6 answers
Thu 2022/04/14
DFA In COQ
5 answers
Wed 2022/04/13
The Coq Club mailing list
Second CfP: FM 2023 - 25th International Symposium on Formal Methods
Mon 2022/05/23
TYPES 2022 -- Second call for participation
Fri 2022/05/20
Call for Papers: Workshop on Type-Driven Development (TyDe)
Fri 2022/05/20
JFLA 2022 -- second appel à participation et précisions sur l'inscription
Fri 2022/05/20
ChoiceType for Coq Type with Field Axioms
Thu 2022/05/19
Experience with formalising projects with length indexed vector (Vector.t) and finite type (Fin.t)
8 replies
Tue 2022/05/17
2nd CfP (deadline 27 May): Autumn school "Proof and Computation" 2022
Tue 2022/05/17
CiE 2022 Call for Participation
Tue 2022/05/17
ML Family Workshop 2022: Final Call for Presentations
Tue 2022/05/17
Lamport on TLA+ in Quanta, with Coq mention
3 replies
Tue 2022/05/17
Zulip
(
archive
)
Notation in custom entry
meaning of fix
Coq as symbolic algebra or symbolic computation program
how portable are .vo files?
Importing functions/lemmas from one Coq file to another?
Unique indices in list
moduls
List formation
Latex and coqdoc
Nat counting
Proof Assistants Stack Exchange
Recursive notations with forall quantifier
Fri 2022/05/20
SSReflect tuple constructor: why not use phantom?
Sun 2022/05/15
Unfolding expressions in Coq by one layer
Sat 2022/05/14
I'm stuck trying to prove ∀x : ℕ, 3 | (x + 5x) with Coq
4 answers
Fri 2022/05/13
How do Coq's bidirectionality hints (`&`) affect type checking?
Thu 2022/05/12
Calculus of (inductive) Constructions: Do inductive definitions increase proof strength?
3 answers
Wed 2022/05/11
How to extract the witness from exists in Coq in function notation/without destructing?
3 answers
Mon 2022/05/02
Coq defining a hierarchy of collections of integers with infinitely many "levels"
1 answer
Sun 2022/05/01
Display style proofs using Coq
Sat 2022/04/30
Tactic unification vs evarconv in Coq
Sat 2022/04/30
Stack Overflow
User defined language in pandoc code-block
Tue 2022/05/24
It is necessary to solve the problem of formal verification in "Coq"
Mon 2022/05/23
Proofs of simple arithmetic expressions
1 answer
Mon 2022/05/23
is coq match statement exhaustive?
1 answer
Mon 2022/05/23
How do I show that if a hypothesis implies not, it's the same as saying the proposition equals false (coq)?
1 answer
Sat 2022/05/21
Coq - trivial induction on lists doesn't accept assumtion
Sat 2022/05/21
The reference info was not found in the current environment
1 answer
Fri 2022/05/20
Running prover in why3 ,using coq - error
Fri 2022/05/20
How to evaluate square of a binom in coq?
2 answers
Fri 2022/05/20
Add an assertion and its negation to Coq
1 answer
Thu 2022/05/19
CS Theory Stack Exchange
Defining functions on non-inductive types using LEM in Coq
1 answer
Fri 2022/01/21
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
Reddit
The reference info was not found in the current environment.
2 comments
Thu 2022/05/19
Coq make failing on Omega
2 comments
Thu 2022/05/19
Type Theory Forall Episode #17 The Lost Elegance of Computation - Conal Elliott
Tue 2022/05/10
Hey, at risk of making a tired question, I could use a little help with something that I'm finding myself stuck on as an of-two-days proof assistant and Coq user. ∀x : ℕ, 3 | (x + 5x). Specifically, what's got me is showing that ∀x y z : ℕ, (z|x and z|y) -> z|(x + y). Attempt in post body.
8 comments
Mon 2022/05/09
Got stuck in proving the malloc/free example
Sat 2022/05/07
Need help in proving logical statement.
5 comments
Fri 2022/05/06
Adding a Field
1 comment
Wed 2022/04/27
Coq Hexadecimal Addition
1 comment
Tue 2022/04/19
Type Theory Forall Episode 16 - Agda, K Axiom, HoTT, Rewrite Theory - Guest: Jesper Cockx
5 comments
Sat 2022/04/02
It's a stupid question but I'm planning to buy x1 carbon for development but I'm not sure 16gb would be enough for coq development
4 comments
Fri 2022/04/01
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
