About the Miscellaneous category


1

649

February 12, 2019

Are dependent types necessary for modelling F Omega


0

43

September 6, 2024

Why are then no clearlyvisible signs of the Coq>Rocq rename?


4

286

July 5, 2024

Looking for Advice on Codifying Theoretical Math in Coq


1

34

July 4, 2024

Why Am I Unable to See My Post?


1

63

July 4, 2024

Coq's Cumulativity


2

63

June 22, 2024

Old Critical Bug described as affecting virtual machine but also triggers on other conversion machines


4

106

June 5, 2024

Proof verifier design


3

105

May 19, 2024

Coqide: What settings can I set in the gtk.css?


3

135

May 9, 2024

Developing a proven, secure communication protocol from scratch


5

609

April 10, 2024

ChatGPT can help translate between Coq and Lean


0

227

February 13, 2024

Notes from the CoqPL 2024 Q/A session


9

546

January 29, 2024

Is there a full documentation of Coq's grammar?


15

2429

December 18, 2023

How do each of the three main lambda calculus features impact what coq can represent?


4

392

October 20, 2023

Is it possible to get parentheses' positions or an operator's associativity from an AST?


3

330

August 27, 2023

Why is Coq consistent? What is the intended semantics?


21

3833

September 27, 2019

Need coq tutor


2

530

April 22, 2023

Finding Coq Freelancers


2

436

April 14, 2023

What is the tag for menhir for coq 8.12 when installing it with opam install y?


3

516

February 17, 2023

Indefinite description axiom could be simpler?


6

570

October 28, 2022

Coq to Why3: Proof of aux lemma of function correction


1

687

August 20, 2022

Learning Real Analysis and Measure Theory together with Coq


6

1801

June 10, 2022

Does Coq have egraphs (for Dependent Types)?


1

582

April 13, 2022

Why doesn't Coq assume UIP or Univalence for equality?


6

971

April 7, 2022

Can you avoid positivity issues with indexing?


1

520

February 20, 2022

Is there any (general) formalization of abstract interpretation?


6

1158

February 15, 2022

What is the runtime of Coq's (dependent) Type Inference?


8

1457

January 18, 2022

Change of default locality for Hint commands in Coq 8.13


13

2701

November 24, 2021

Ask For Basic Commands For COQ


15

1588

September 8, 2021

Does proof of coq consistency need axiom of choice?


3

1080

February 6, 2020
