Confused about hierarchies of functions


0

520

August 9, 2021

Finite types, historical question


2

721

July 7, 2021

Coqclub archive is off?


5

739

July 5, 2021

Coq to Why3: Proof of function correction


1

613

June 21, 2021

Coq to Why3: with notation


1

666

June 18, 2021

How do regular and exact completions fit into Coq's use of setoids?


4

724

June 7, 2021

Can every theorem that has a proof be completed without DSL tactics?


9

1171

January 13, 2021

Visualizing contributions to the Coq implementation and all Coq opam packages


7

1054

May 18, 2021

Formalized Divideandconquer for Lists


0

653

April 30, 2021

Nix package for coq theories with dependencies


2

1095

March 31, 2021

What does it mean that Isabelle has better automation than Coq?


15

4292

March 25, 2021

Cite Coq Library Materials


0

655

January 16, 2021

"Mainstream" programming systems with a Coqlike development style?


2

736

January 5, 2021

Starting to learn coq


8

1222

November 23, 2020

Why are proof assistants used mostly to catch bugs instead of using it to truly proving correctness?


4

1024

September 4, 2020

How is Coq (or any Proof Assistants) used to for hardware verification?


1

1039

August 31, 2020

Listing and preserving formalized mathematical results in Coq


0

711

August 30, 2020

Proof By Induction On Lists


1

646

August 14, 2020

Coq trusted kernel code size


1

1127

August 10, 2020

Are there any declarative proof languages for Coq?


4

1961

August 7, 2020

How does one generate a static proof trees of a whole Coq Proof?


2

906

August 6, 2020

Can one translate from one ITP language to another automatically?


5

1024

August 6, 2020

What are the arguments of a function that computes the steps of a theorem (assuming the theorem has a proof)?


7

808

August 6, 2020

List of statements for verifying ATPs


2

603

August 6, 2020

Kevin Buzzard's intervention: Where is the fashionable mathematics? (Lean etc.)


1

685

August 3, 2020

What do we need to be able to compute reverse tactics application?


6

696

July 21, 2020

What is the difference between SSReflect and Czar?


12

1887

July 20, 2020

How to make verified software more accessible


9

1495

July 9, 2020

Would Coq benefit from docstrings?


7

1546

May 27, 2020

Why dependent type theory?


51

4989

May 14, 2020
