About the Miscellaneous category


2

141

February 12, 2019

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


5

139

September 4, 2020

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


2

89

August 31, 2020

Listing and preserving formalized mathematical results in Coq


1

104

August 30, 2020

Proof By Induction On Lists


2

74

August 14, 2020

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


15

271

August 14, 2020

Coq trusted kernel code size


2

102

August 10, 2020

Are there any declarative proof languages for Coq?


5

162

August 7, 2020

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


3

74

August 6, 2020

Can one translate from one ITP language to another automatically?


6

101

August 6, 2020

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


7

117

August 6, 2020

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


8

118

August 6, 2020

List of statements for verifying ATPs


3

139

August 6, 2020

Is there a full documentation of Coq's grammar?


11

269

August 6, 2020

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


2

158

August 3, 2020

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


7

92

July 21, 2020

What is the difference between SSReflect and Czar?


13

224

July 20, 2020

How to make verified software more accessible


10

185

July 9, 2020

Would Coq benefit from docstrings?


8

251

May 27, 2020

Why dependent type theory?


52

883

May 14, 2020

[Coq Discourse] Code listings broken in mailing list mode


3

84

March 26, 2020

Re: Coq vs lean for classical analysis


2

173

February 24, 2020

Suggestions for bachelor thesis


4

206

February 12, 2020

Any resources for those studying Software Foundations on their own?


6

262

February 7, 2020

Does proof of coq consistency need axiom of choice?


4

267

February 6, 2020

Proof on normalization of CIC and its consistency


5

438

January 30, 2020

Any formally verified open source libraries?


13

463

December 25, 2019

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


5

459

December 24, 2019

High assurance / high code complexity use of Coq


17

692

December 4, 2019

Why is Coq consistent? What is the intended semantics?


22

1184

September 27, 2019
