Link aggregator of discussions about the
interactive theorem prover
Bug in universe inference?
Stuck at Multiset.v contents_cons_inv
Ad hoc asynchronicity
Next CUDW 2020/11/30 to 2020/12/04 — Save the Date!
Why induction principle such as list_rect cannot be added in Hint database?
Trying to prove sort algorithm correctness (for specific n), in search for hints
Announcing Coq 8.12 support for Codewars
Inserting PPX annotations into extracted OCaml
Pattern matching: warn unused parameter?
The Coq Club mailing list
Faculty position at Portland State University
Need help making a modular reflection reifier
ICALP 2021 Call for Workshops
CADE-28: Call for Papers, Workshops, Tutorials and Competitions
CADE-28 Call for Papers, Workshops, Tutorials, Competitions
ITP 2021: Call for Papers
Research position in Formal Verification (m/f/x) at HENSOLDT Cyber in Munich
LICS 2021 Call for Papers
F-IDE 2021 - Call for Papers
LICS 2021 Call for Workshops
"Abstraction barriers" in software foundations
Tactics intro for dependently typed programmer?
Custom induction principle for inductive proposition
Using Coq with VScode under windows 10
`pattern` tactic and goals with dependencies
Record with class instances?
ssr confusing intro pattern
Minimze bugs without github comment?
Opam and library for new users
Equality on complex functions with complex type
Automatically proving a non-linear arithmetic proposition over Z in Coq
Equality on complex functions
Is there a good strategy for proving the given teorem?
How to prove equivalence between those two types - algorithm' and algorithm''?
Z_3: left inversion lemma
Coq unable to unify -- how to change hypothesis?
How to apply a constructor in an hypothesis?
Messing around with category theory
Z_3: left id proof
CS Theory Stack Exchange
An axiom for John Major's Equality
Defining finite sets inductively in a proof assistant?
Has the compactness theorem for FOL been formalized in Coq/Isabelle/etc?
Lack of atomic propositions in the Calculus of Constructions from ATTAPL textbook
Journals or conferences to submit formally verified libraries?
On the interpretation of coinduction in type theory
Have the proofs in Buss's "On Goedel’s Theorems on Lengths of Proofs" been formalized (mechanically checked)?
Proposition terms vs types in Coq
Prove proof irrelevance in Coq?
Model of Coq (pCuIC) in higher toposes?
Is it normal to complete a proof without really knowing what's going on?
ANSSI released reviewing standards for Coq proofs placing Coq at the highest (EAL7) level for software verification
Interfacing with Coq
A Series on Ltac
Proving things about bool functions
Some proofs about sequences and series
New Software Foundations volume: "Verifiable C" by Appel and Cao
Program Logics for Certified Compilers
Installation -- HELP!
Coq 8.12.0 is out
Coq 8.12+beta1 is out
Coq 8.11.2 is out
Coq 8.11.1 is out
Coq 8.11.0 is out
Coq 8.11+beta1 is out
Coq 8.10.2 is out
Coq 8.10.1 is out
Coq 8.10.0 is out
Coq 8.10+beta3 is out