About the Miscellaneous category


1

149

February 12, 2019

Starting to learn coq


8

54

November 23, 2020

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


4

177

September 4, 2020

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


1

115

August 31, 2020

Listing and preserving formalized mathematical results in Coq


0

121

August 30, 2020

Proof By Induction On Lists


1

93

August 14, 2020

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


14

396

August 14, 2020

Coq trusted kernel code size


1

135

August 10, 2020

Are there any declarative proof languages for Coq?


4

203

August 7, 2020

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


2

88

August 6, 2020

Can one translate from one ITP language to another automatically?


5

116

August 6, 2020

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


6

133

August 6, 2020

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


7

133

August 6, 2020

List of statements for verifying ATPs


2

153

August 6, 2020

Is there a full documentation of Coq's grammar?


10

344

August 6, 2020

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


1

180

August 3, 2020

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


6

110

July 21, 2020

What is the difference between SSReflect and Czar?


12

274

July 20, 2020

How to make verified software more accessible


9

240

July 9, 2020

Would Coq benefit from docstrings?


7

317

May 27, 2020

Why dependent type theory?


51

1105

May 14, 2020

[Coq Discourse] Code listings broken in mailing list mode


2

97

March 26, 2020

Re: Coq vs lean for classical analysis


1

292

February 24, 2020

Suggestions for bachelor thesis


3

226

February 12, 2020

Any resources for those studying Software Foundations on their own?


5

327

February 7, 2020

Does proof of coq consistency need axiom of choice?


3

301

February 6, 2020

Proof on normalization of CIC and its consistency


4

487

January 30, 2020

Any formally verified open source libraries?


12

539

December 25, 2019

Why doesn't Coq have a theorem Type like HOL Light?


4

543

December 24, 2019

High assurance / high code complexity use of Coq


16

750

December 4, 2019
