About the Miscellaneous category


1

596

February 12, 2019

Developing a proven, secure communication protocol from scratch


5

503

April 10, 2024

ChatGPT can help translate between Coq and Lean


0

119

February 13, 2024

Notes from the CoqPL 2024 Q/A session


9

345

January 29, 2024

Is there a full documentation of Coq's grammar?


15

2214

December 18, 2023

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


4

272

October 20, 2023

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


3

220

August 27, 2023

Why is Coq consistent? What is the intended semantics?


21

3477

September 27, 2019

Need coq tutor


2

429

April 22, 2023

Finding Coq Freelancers


2

372

April 14, 2023

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


3

381

February 17, 2023

Indefinite description axiom could be simpler?


6

500

October 28, 2022

Coq to Why3: Proof of aux lemma of function correction


1

605

August 20, 2022

Learning Real Analysis and Measure Theory together with Coq


6

1646

June 10, 2022

Does Coq have egraphs (for Dependent Types)?


1

490

April 13, 2022

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


6

810

April 7, 2022

Can you avoid positivity issues with indexing?


1

464

February 20, 2022

Is there any (general) formalization of abstract interpretation?


6

1048

February 15, 2022

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


8

1314

January 18, 2022

Change of default locality for Hint commands in Coq 8.13


13

2499

November 24, 2021

Ask For Basic Commands For COQ


15

1417

September 8, 2021

Does proof of coq consistency need axiom of choice?


3

1031

February 6, 2020

Confused about hierarchies of functions


0

441

August 9, 2021

Finite types, historical question


2

639

July 7, 2021

Coqclub archive is off?


5

676

July 5, 2021

Coq to Why3: Proof of function correction


1

500

June 21, 2021

Coq to Why3: with notation


1

573

June 18, 2021

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


4

651

June 7, 2021

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


9

1066

January 13, 2021

Visualizing contributions to the Coq implementation and all Coq opam packages


7

941

May 18, 2021
