Planet Coq
Link aggregator of discussions about the
Coq
interactive theorem prover
Discourse
Ocaml native int63 extraction
Tue 2023/10/03
Coq manual build with dune
2 answers
Thu 2023/09/28
Permanent Post [L/SL] in Applied Formal Methods at Swansea University
Thu 2023/09/28
PhD Position in formal proofs @LMF/Université Paris-Saclay
Thu 2023/09/28
(2nd CfP) Dafny Workshop at POPL 24
Wed 2023/09/27
CertiuCOS2
Mon 2023/09/25
An inductive definition failed with error "Non strictly positive occurrence..."
6 answers
Fri 2023/09/22
[VsCoq Legacy] Release
Wed 2023/09/20
[VsCoq 2] Patch Release 2.0.1
Wed 2023/09/20
Coq Platform 2023.03.0 release with Coq 8.17.1
Mon 2023/09/18
The Coq Club mailing list
Proving transitiviy of simple type system
10 replies
Tue 2023/10/03
PLDI 2024 Call for Papers
Tue 2023/10/03
PADL'24: Last Call for Papers
Mon 2023/10/02
unification ignores local evar let bindings
Mon 2023/10/02
ETAPS 2024 final joint call for papers
Fri 2023/09/29
1+2=3 via functorial programming — Bing AI's re: [ALGTOP-L] Support Needed to Save Math at WVU
Fri 2023/09/29
match on multiple goals simultaneously
1 reply
Thu 2023/09/28
(2nd CfP) Dafny Workshop at POPL 24
Wed 2023/09/27
APLAS 2023: Call for Participation
Mon 2023/09/25
2nd Call for Papers Proceedings for ThEdu'23 - Theorem Proving Components for Educational Software
Mon 2023/09/25
Zulip
(
archive
)
✔ Coq.Sets.Ensembles inhabited
Extensive form games, how to formalize information sets?
Ltac1 reference:()
Matrix transpose
Passing an ltac thunk to a tactic notation?
Minimal working examples of Coq code
Online documentation broken?
"Anomaly "conversion was given unreduced term (FLambda)." wi
✔ greater than relation
Release of Std++ for 8.18
Proof Assistants Stack Exchange
How do I write a minimal working example (MWE) in Coq to demonstrate some problem?
Tue 2023/10/03
Formalization of a model of ∞-category in a proof assistant
2 answers
Tue 2023/10/03
Eta-equality for records: the case of semigroups
1 answer
Mon 2023/10/02
gappa seems to generate bad Coq
1 answer
Fri 2023/09/29
Debug autorewrite in Coq
1 answer
Wed 2023/09/27
iris/algebra/auth.vo has bad version number 81700 (expected 81601) for IRIS Coq
1 answer
Tue 2023/09/26
How to prove basic lemmas about divisibility in Coq?
2 answers
Sun 2023/09/24
Rewriting with heterogeneous equality (JMeq)
1 answer
Fri 2023/09/22
Dependent sum and equality with Coq
2 answers
Tue 2023/09/19
(Dis)Advantages of basing a proof assistant on CH correspondence?
1 answer
Tue 2023/09/19
Stack Overflow
Coq matrix manipulation
1 answer
Tue 2023/10/03
Software Foundations Basics - Theorem lower_grade_lowers need to prove implication Eq = Lt -> Eq = Lt
2 answers
Fri 2023/09/29
coq, is there a tartic to auto solve simle inequality such as a < b for real numbers?
Thu 2023/09/21
Cannot infer the type of function in environment
1 answer
Wed 2023/09/20
vscoq language server failed installing
Thu 2023/09/14
How to represent 2D array in Verifiable C
1 answer
Tue 2023/09/12
Understanding TLC's finite map library
Tue 2023/09/12
How to proof by natural number case analysis in Coq?
3 answers
Sun 2023/09/10
false = true problem when solving Lemma in Coq
2 answers
Wed 2023/08/30
How to install Coq
2 answers
Tue 2023/08/29
CS Theory Stack Exchange
Formalization of matching logic (logic behind K Framework)
3 answers
Wed 2023/08/16
Notation problem
1 answer
Thu 2023/06/01
Can I define nested mutually dependent types in Coq?
1 answer
Sat 2023/05/13
Defining finite sets inductively in a proof assistant?
1 answer
Tue 2023/04/25
Yet another constructive (Coq) proof that `nat -> nat -> nat` is not bijective. How to explain it to myself?
3 answers
Thu 2023/03/23
Why does Coq have Prop?
4 answers
Fri 2022/12/09
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
Reddit
Help with Inductive Relations
1 comment
Thu 2023/10/05
Help with Transitive Closure
2 comments
Tue 2023/10/03
I am unable to understand Structured Data
4 comments
Mon 2023/10/02
Software Foundations - confused with applying destruct on Prop
9 comments
Fri 2023/09/22
Lean/Coq/Isabel and Their Proof Trees
Thu 2023/09/21
On Extraction of Coq Programs
4 comments
Thu 2023/09/21
Formally verified WebAssembly using Coq and Extism
Tue 2023/09/12
Type Theory Forall Podcast #33 Z3 and Lean, the Spiritual Journey - Leo de Moura
2 comments
Sat 2023/09/09
How do we derive the 'match ... with' thing in pure CIC?
3 comments
Thu 2023/08/31
I dont understand the coding of AND and OR in type theory (the intuitive explanation)
1 comment
Sat 2023/08/26
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
