Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Constructing heterogeneous lists
4 answers
Tue 2021/10/26
Thinking of using hammer/automation to guide the order of proving lemmas
Sun 2021/10/24
Notation for a coinductive type
Fri 2021/10/22
Importing with aliasing
2 answers
Sat 2021/10/16
Definitions completed with proof scripts are opaque, how to make them compute
2 answers
Fri 2021/10/15
Instances created with ':= ltac:(_)' are much slower than Definitions
1 answer
Fri 2021/10/15
Coq 8.15 branch date
Thu 2021/10/14
Newbie Needs Tutor on ZOOM
1 answer
Thu 2021/10/14
Does Universe Polymorphism extend the theory of Coq?
5 answers
Fri 2021/10/01
Overload list notation
3 answers
Mon 2021/09/27
The Coq Club mailing list
Ran Ettinger's tutorial on using Dafny to teach: FME Teaching Committee's Tutorial Series, October edition
Tue 2021/10/26
π>e
10 replies
Mon 2021/10/25
LICS 2022 Call for Papers
Fri 2021/10/22
Engineer positions for the ProofInUse consortium
Fri 2021/10/22
Typechecker is running for 20 minutes, with 100% cpu and without any output
Fri 2021/10/22
Assistant Professor position in Formal Methods, Eindhoven University, The Netherlands
Thu 2021/10/21
PhD position in Type Theory at Chalmers/Gothenburg University (deadline 8 Nov)
Thu 2021/10/21
Proof Society Workshop and Winter School 2021
Thu 2021/10/21
ICLP 2022 Call For Papers
Thu 2021/10/21
TYPES 2021 post-proceedings: Open call for papers
Tue 2021/10/19
Zulip
logical foundations
Towards a CEP for improving Search
Typeclass resolution looping, yet not searching?
stdpp: build a map from a list of pairs
Importing a library using NixOS
induction on n
Update values
Beginner: SF question
How can I define ODE (ordinary differential equation)?
Termination checking rules
Stack Overflow
Decidable equality statement with Set vs. Prop
1 answer
Mon 2021/10/25
How to do induction on BinNums.Z in Coq/
2 answers
Mon 2021/10/25
How to have multiple notations of "0" in Coq
1 answer
Mon 2021/10/25
Real numbers in Coq
2 answers
Sat 2021/10/23
Why does an "only printing" notation modify the parser
1 answer
Fri 2021/10/22
Coq Error: Illegal application (Non-functional construction)
1 answer
Wed 2021/10/20
Proof in Coq with named parameters in constructors
1 answer
Tue 2021/10/19
Coercions of bitvectors
Tue 2021/10/19
Coq: why do I need to manually unfold a value even though it has a `Hint Unfold` on it?
2 answers
Tue 2021/10/19
Proving that s-expressions printing is injective
1 answer
Mon 2021/10/18
CS Theory Stack Exchange
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
An axiom for John Major's Equality
Tue 2021/01/19
Defining finite sets inductively in a proof assistant?
1 answer
Tue 2020/05/05
Reddit
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?
2 comments
Sun 2021/09/05
Slides & Videos of the Coq Workshop 2021
Mon 2021/08/30
Is Coq’ Art book still worth it?
6 comments
Wed 2021/08/11
Clashing versions of ocaml on cpdt text compile
4 comments
Tue 2021/08/10
Join together types
2 comments
Fri 2021/08/06
Simple Example of Inductive
5 comments
Tue 2021/06/22
Proving a function body of an Abstract Data Type
3 comments
Mon 2021/05/31
Proving that [insert] produces a Binary Search Tree
5 comments
Sat 2021/05/22
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
