Listing and preserving formalized mathematical results in Coq


0

445

August 30, 2020

Proof By Induction On Lists


1

426

August 14, 2020

Coq trusted kernel code size


1

686

August 10, 2020

Are there any declarative proof languages for Coq?


4

1234

August 7, 2020

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


2

466

August 6, 2020

Can one translate from one ITP language to another automatically?


5

600

August 6, 2020

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


7

467

August 6, 2020

List of statements for verifying ATPs


2

418

August 6, 2020

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


1

504

August 3, 2020

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


6

394

July 21, 2020

What is the difference between SSReflect and Czar?


12

1077

July 20, 2020

How to make verified software more accessible


9

923

July 9, 2020

Would Coq benefit from docstrings?


7

1024

May 27, 2020

Why dependent type theory?


51

3216

May 14, 2020

[Coq Discourse] Code listings broken in mailing list mode


2

378

March 26, 2020

Re: Coq vs lean for classical analysis


1

1329

February 24, 2020

Suggestions for bachelor thesis


3

578

February 12, 2020

Any resources for those studying Software Foundations on their own?


5

895

February 7, 2020

Proof on normalization of CIC and its consistency


4

1422

January 30, 2020

Any formally verified open source libraries?


12

1437

December 25, 2019

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


4

1571

December 24, 2019

High assurance / high code complexity use of Coq


16

1510

December 4, 2019

Why is Coq consistent? What is the intended semantics?


21

2504

September 27, 2019

What does « .v » stand for?


1

480

September 14, 2019

Should other languages than English be allowed on the Discourse forum?


46

2385

September 12, 2019

Maintainers of Coquille plugin for Vim  please check the pull requests


4

797

August 28, 2019

Why is ηreduction illegal?


2

549

August 1, 2019

Is "induction" polysemic?


1

820

March 21, 2019

Is Coq able to prove the identity x = x for infinite precision real numbers?


11

1759

March 12, 2019

Syntax highlighting on Discourse


3

509

March 4, 2019
