Link aggregator of discussions about the
interactive theorem prover
Ocaml native int63 extraction
Coq manual build with dune
Permanent Post [L/SL] in Applied Formal Methods at Swansea University
PhD Position in formal proofs @LMF/Université Paris-Saclay
(2nd CfP) Dafny Workshop at POPL 24
An inductive definition failed with error "Non strictly positive occurrence..."
[VsCoq Legacy] Release
[VsCoq 2] Patch Release 2.0.1
Coq Platform 2023.03.0 release with Coq 8.17.1
The Coq Club mailing list
Proving transitiviy of simple type system
PLDI 2024 Call for Papers
PADL'24: Last Call for Papers
unification ignores local evar let bindings
ETAPS 2024 final joint call for papers
1+2=3 via functorial programming — Bing AI's re: [ALGTOP-L] Support Needed to Save Math at WVU
match on multiple goals simultaneously
(2nd CfP) Dafny Workshop at POPL 24
APLAS 2023: Call for Participation
2nd Call for Papers Proceedings for ThEdu'23 - Theorem Proving Components for Educational Software
✔ Coq.Sets.Ensembles inhabited
Extensive form games, how to formalize information sets?
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?
Formalization of a model of ∞-category in a proof assistant
Eta-equality for records: the case of semigroups
gappa seems to generate bad Coq
Debug autorewrite in Coq
iris/algebra/auth.vo has bad version number 81700 (expected 81601) for IRIS Coq
How to prove basic lemmas about divisibility in Coq?
Rewriting with heterogeneous equality (JMeq)
Dependent sum and equality with Coq
(Dis)Advantages of basing a proof assistant on CH correspondence?
Coq matrix manipulation
Software Foundations Basics - Theorem lower_grade_lowers need to prove implication Eq = Lt -> Eq = Lt
coq, is there a tartic to auto solve simle inequality such as a < b for real numbers?
Cannot infer the type of function in environment
vscoq language server failed installing
How to represent 2D array in Verifiable C
Understanding TLC's finite map library
How to proof by natural number case analysis in Coq?
false = true problem when solving Lemma in Coq
How to install Coq
CS Theory Stack Exchange
Formalization of matching logic (logic behind K Framework)
Can I define nested mutually dependent types in Coq?
Defining finite sets inductively in a proof assistant?
Yet another constructive (Coq) proof that `nat -> nat -> nat` is not bijective. How to explain it to myself?
Why does Coq have Prop?
What exactly is "large elimination"?
A Coq question : How to prove the image of the two same valued variables under a function are same?
Defining functions on non-inductive types using LEM in Coq
Prove proof irrelevance in Coq?
Help with Inductive Relations
Help with Transitive Closure
I am unable to understand Structured Data
Software Foundations - confused with applying destruct on Prop
Lean/Coq/Isabel and Their Proof Trees
On Extraction of Coq Programs
Formally verified WebAssembly using Coq and Extism
Type Theory Forall Podcast #33 Z3 and Lean, the Spiritual Journey - Leo de Moura
How do we derive the 'match ... with' thing in pure CIC?
I dont understand the coding of AND and OR in type theory (the intuitive explanation)
Coq Platform 2021.02.0 is out
Coq 8.13.1 is out
Coq 8.13.0 is out
Coq 8.12.2 is out
Coq 8.13+beta1 is out
Coq 8.12.1 is out
Coq 8.12.0 is out
Coq 8.12+beta1 is out
Coq 8.11.2 is out
Coq 8.11.1 is out