About the Miscellaneous category


1

579

February 12, 2019

ChatGPT can help translate between Coq and Lean


0

65

February 13, 2024

Notes from the CoqPL 2024 Q/A session


9

243

January 29, 2024

Is there a full documentation of Coq's grammar?


15

2116

December 18, 2023

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


4

219

October 20, 2023

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


3

193

August 27, 2023

Developing a proven, secure communication protocol from scratch


2

408

July 10, 2023

Why is Coq consistent? What is the intended semantics?


21

3362

September 27, 2019

Need coq tutor


2

381

April 22, 2023

Finding Coq Freelancers


2

330

April 14, 2023

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


3

329

February 17, 2023

Indefinite description axiom could be simpler?


6

444

October 28, 2022

Coq to Why3: Proof of aux lemma of function correction


1

558

August 20, 2022

Learning Real Analysis and Measure Theory together with Coq


6

1550

June 10, 2022

Does Coq have egraphs (for Dependent Types)?


1

450

April 13, 2022

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


6

752

April 7, 2022

Can you avoid positivity issues with indexing?


1

430

February 20, 2022

Is there any (general) formalization of abstract interpretation?


6

977

February 15, 2022

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


8

1238

January 18, 2022

Change of default locality for Hint commands in Coq 8.13


13

2387

November 24, 2021

Ask For Basic Commands For COQ


15

1333

September 8, 2021

Does proof of coq consistency need axiom of choice?


3

1002

February 6, 2020

Confused about hierarchies of functions


0

408

August 9, 2021

Finite types, historical question


2

587

July 7, 2021

Coqclub archive is off?


5

640

July 5, 2021

Coq to Why3: Proof of function correction


1

455

June 21, 2021

Coq to Why3: with notation


1

514

June 18, 2021

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


4

620

June 7, 2021

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


9

1011

January 13, 2021

Visualizing contributions to the Coq implementation and all Coq opam packages


7

874

May 18, 2021
