Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Coq Hackaton Winter 2022 edition
2 answers
Sat 2022/01/22
Prooving the length of a list under constraint
4 answers
Sat 2022/01/22
Coq QuickChick : Making propery Checkable, Decidable, Arbitrary (Gen)
2 answers
Thu 2022/01/20
MathComp 1.14.0 released
Wed 2022/01/19
QuickChick : forAll and forAllShrink for binary functions
1 answer
Tue 2022/01/18
What is the runtime of Coq's (dependent) Type Inference?
8 answers
Tue 2022/01/18
Difference between P -> Q and P /\ Q
7 answers
Mon 2022/01/17
V8.15.0 tag set
Thu 2022/01/13
Confused about nested inductive coinductive types
3 answers
Tue 2021/12/21
Html/PDF documentation building with dune
1 answer
Thu 2021/12/16
The Coq Club mailing list
Release of Lambdapi 2.1.0
Thu 2022/01/20
MathComp 1.14.0 released
Wed 2022/01/19
[CfP] ICLP 2022 - Deadline Extension (28th Jauary)
Tue 2022/01/18
FSCD 2022: Second Call for Papers
Tue 2022/01/18
[ANN] Coq Hackaton Winter 2022 edition
Mon 2022/01/17
: optimized Regexp Library
1 reply
Mon 2022/01/17
Multiple Research Fellow positions at the Australian National University
Mon 2022/01/17
Postdoc positions on Formal Verification for Zero-Trust IoT Systems at Kyoto University and National Institute of Informatics (NII), Japan
Fri 2022/01/14
PLP 2022: The 9th Workshop on Probabilistic Logic Programming
Thu 2022/01/13
[Final CfP] ICLP 2022 - The 38th International Conference on Logic Programming
Thu 2022/01/13
Zulip
(
archive
)
coqtop xml protocol example
Coq's Winter 2022 Hackaton
list of points
Hypothesis statement
Can I create alias when importing
How to apply `Wf_Z.natlike_ind`?
CoqPL is on Saturday, again
✔ meta.yml and mustache
ITP
Where `strream` is defined?
Stack Overflow
How to prove an absurd rule in Coq
1 answer
Sat 2022/01/22
How to prove the correction of derive on reg_exp
1 answer
Tue 2022/01/18
Coq - Coercion of list nat
1 answer
Sun 2022/01/16
Is it possible to remove/override an existing coercion?
1 answer
Sun 2022/01/16
Why Coq does not infer the type parameter
1 answer
Fri 2022/01/14
Relations with dependent types in Coq
1 answer
Thu 2022/01/13
How do you define an ordered pair in Coq?
1 answer
Wed 2022/01/12
Coq QuickChick : Making propery Checkable, Decidable, Arbitrary (Gen)
1 answer
Sun 2022/01/09
How can I write a tactic which works both in a goal and a hypothesis?
1 answer
Sat 2022/01/08
How to prove shorter nat comparisons like 10000 > 1 for sigma types in Coq?
3 answers
Fri 2022/01/07
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
Error Compiling Software Foundations Volume 5
6 comments
Sun 2022/01/02
Type Theory Forall Podcast #13 - C/C++, Emacs, Haskell, and Coq. The Journey (John Wiegley)
Thu 2021/12/23
On relational compilation
Wed 2021/12/08
Help the Proof Assistants Stack Exchange reach Beta!
1 comment
Sun 2021/11/21
The proposal for a proof assistants StackExchange site
Sat 2021/11/20
On proving lists infinite
Tue 2021/10/26
A Verified Online Monitor for Metric Temporal Logic with Quantitative Semantics
3 comments
Fri 2021/10/01
Formal verification manager job at Google - Coq experience a plus
1 comment
Thu 2021/09/23
New to Coq: How to compile .vo files and run command line?
3 comments
Sun 2021/09/05
Slides & Videos of the Coq Workshop 2021
Mon 2021/08/30
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
