Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Coq 8.16.1 has been tagged
Fri 2022/11/25
MathComp Workshop and Winter School (Dec 5-9 2022) - last call
Fri 2022/11/18
Branching v8.17 soon
Wed 2022/11/16
ProofGeneral release 4.5
1 answer
Tue 2022/11/15
Type (let (a, b) = ... in something a) vs. (something (let (a, b) = ... in a))
5 answers
Tue 2022/11/08
Interval 4.6, now with decimal enclosures and floating-point rounding operators
Thu 2022/10/27
Is it possible to share binary-only libraries across OSes?
5 answers
Wed 2022/10/19
Postdoc and Internship positions at IBM Research
Fri 2022/10/14
PhD/postdoc vacancy on the verification of cryptographic protocols at Aarhus University
Wed 2022/10/12
MathComp Workshop and Winter School (Dec 5-9 2022) - second call
Wed 2022/10/12
The Coq Club mailing list
ICFP 2023: Call for Workshop and Co-Located Event
Thu 2022/12/01
Dov Gabbay Prize for Logic and Foundations
Wed 2022/11/30
[14-12-2022] Workshop on Dependent Type Theory in Nantes
1 reply
Wed 2022/11/30
FSCD-CADE 2023: Call for Workshop Proposals
Tue 2022/11/29
Call for Participation: POPL'23
Tue 2022/11/29
FSCD 2023: First Call for Papers
Mon 2022/11/28
Tenure Track Assistant Professor - The University of Kansas
Mon 2022/11/28
order-independent .vo files
2 replies
Sun 2022/11/27
Fully funded PhD positions in PL theory and interactive theorem proving at Heriot-Watt University in Edinburgh
Wed 2022/11/23
Proposals for Sites for IJCAR 2024
Mon 2022/11/21
Zulip
(
archive
)
Controlling printing notations
Using HoTT Library
✔ A PHOAS example
Induction Principal for Set, represented by list.
No of elements
Change, but with evars
✔ beginners question on induction
Coq gets killed
Some Coq servers down
Combining typeclasses and recursion
Proof Assistants Stack Exchange
Cannot open pixbuf loader module file in Windows
Mon 2022/11/21
Applying custom tactic in hypothesis
1 answer
Thu 2022/11/17
Why are these two proofs so different?
2 answers
Wed 2022/11/16
How does one translate Lean to Coq (and visa versa)?
1 answer
Fri 2022/11/11
Coq ssreflect - rewrite inside \big
1 answer
Tue 2022/11/08
How do I work with ints when using coq-of-ocaml for OCaml to Coq conversion?
1 answer
Thu 2022/11/03
What are the upsides and downsides of typed vs untyped conversion?
2 answers
Sun 2022/10/23
Universe polymorphism and modules in Coq
1 answer
Thu 2022/10/20
How can we formalize a game where each player is a program having access to opponent's code?
2 answers
Sun 2022/10/16
Coq Typeclass on Functions Gets Confused by Equality
Tue 2022/09/27
Stack Overflow
type variable in datatype definition
1 answer
Tue 2022/11/29
How do I exit coqtop REPL?
2 answers
Sun 2022/11/27
Verified software toolchain : which tactic to apply commutativity in mpred
Fri 2022/11/25
Question about failure to match wildcard character "_"
1 answer
Fri 2022/11/25
Big Step Substraction
Thu 2022/11/24
Proving Union of Ensemble is not Empty_set
1 answer
Thu 2022/11/24
Is it possible to convert all higher-order logic and dependent type in Lean/Isabelle/Coq into first-order logic?
1 answer
Sun 2022/11/20
Printing Coq definition without loading library
1 answer
Sat 2022/11/19
Software Foundations: weak_pumping lemma proof
1 answer
Thu 2022/11/17
How can I write a proof to match inductive type without using forall in its subterm?
1 answer
Thu 2022/11/10
CS Theory Stack Exchange
What exactly is "large elimination"?
2 answers
Tue 2022/11/15
A Coq question : How to prove the image of the two same valued variables under a function are same?
1 answer
Sun 2022/07/10
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
Reddit
Boolean Short Circuiting
7 comments
Wed 2022/11/30
Coq vs SMTs
1 comment
Sat 2022/11/19
A Type-Based Approach to Divide-And-Conquer Recursion in Coq [pdf]
4 comments
Thu 2022/11/10
prove DeMorgan law in coq
5 comments
Wed 2022/10/19
How I feel doing software foundations
2 comments
Sat 2022/09/10
Autocompletion in Vim.
6 comments
Mon 2022/09/05
Breaking Badfny
Fri 2022/09/02
How does one access the dependent type unification algorithm from Coq's internals -- especially the one from apply and the substitution solution?
1 comment
Fri 2022/07/15
Type Theory Forall Podcast - Experience Report Learning Coq
Sat 2022/06/04
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
4 comments
Mon 2022/05/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
