Chapter 11 (Flag-style natural deduction in λD) - NaturalDeduction.v

Chapter 12 (Mathematics in λD: a first attempt) - MathematicsFirstAttempt.v

Chapter 13 (Sets and subsets) - SetsAndSubsets.v

I've turned off Coq Standard Library (-noinit option) and everything is developed from scratch and no inductive types are used. I developed a new Coq dialect which is as close to the textbook as possible.

I'm happy to say that the modern version of Coq (2024) is 100% compatible with the original Calculus of Constructions and λD extension. I bet chapters from 2 to 10 is also possible to formalize, so you can keep it in mind if you would like to learn type theory deeper.

I would like to get some code review and suggestions/corrections. Any feedback is good. https://github.com/kciray8/the-great-formalization-project/pull/2/files

Keep in mind though that I decided to save a bit of time by allowing coq automatically name things for me (H0, H1, H2 etc) and haven't done any code refactoring for readability yet.

I didn't see any official announcements anywhere, but it seems like Coq will finally be changing its name to the Rocq Prover.

Between Software Foundations and Adam Chlipala's books, there is an enormous amount of excellent introductory material for "programming in the small" in Coq. On the other hand, whenever I try to write a Coq project of non-trivial size, I run into all sorts of issues. They include:

• When should I use modules vs. typeclasses?

• Is using setoids everywhere instead of eq overkill?

• When should I use reflection?

• When should I use refine?

• When should I use Program (Russell)?

• What options should I set? Implicit Arguments seems to be consensus, are there others?

• What set of libraries should I default to?

...and, while I'm at it, here are some "coding in the small" things I can't figure out:

• How do I make coinduction non-painful?

• How do I use hints properly?

Any insight is greatly appreciated.

I finished reading "To Mock a Mockingbird" by Raymond Smullyan which is an introduction to combinatory logic. I was excited to try my hand at formalizing the proofs using Coq, and this is the result.

Along the way, I even discovered a major, but easily correctible, mistake that Smullyan made. To make certain proofs go through, I also had to prove the Church-Rosser theorem, which seemed to be implicitly taken for granted by Smullyan.

Anyway I just wanted to show off my code here and welcome any suggestions.

It's been 4 years. I don't use Coq, but am curious as to what happened to the renaming.

I recently finished my undergraduate degree in CS. I was lucky enough to work on some research involving formal verification using the Coq proof assistant. This project was submitted to CoqPL and I was lucky enough to give a talk at CoqPL.

I really want to work in formal verification. I am planning on doing a PhD, but will likely apply this fall, and begin next year. I would ideally like to switch roles (from swe) to something more aligned with PL research. I spend most of my free time using Coq for two research projects with various faculty and PhD students.

Does anyone know some companies doing formal verification or PL research, and open to hiring an undergraduate. Any tips / pointers would be awesome!

TY!!

Hey everyone,

I'm experimenting with maintaining a blog for weekly(ish?) Coq puzzles here. My intent is these problems will deal will mostly basic mathematics, and that the challenge comes moreso from the angles of constructivism and/or formalization. I don't intend these to be beginner-level/tutorial type problems, but at the same time you shouldn't have to be a Coq wizard to be able to solve these.

The first problem is up, which you can find here. I'll try to post a solution a few days after a problem is posted.

I'd be happy to hear feedback about format, layout, problem difficulty, or suggestions for future problems. Thanks!

Hi! Me again :]
I'd love to share my progress on tree-sitter-rocq

https://github.com/aruzdh/tree-sitter-rocq

Pre-release 0.2.0 focuses on mirroring some rules from the official reference manual, so anybody who wants to contribute or give it a look can have a better understanding by following the official grammar.

Plus, I'm currently working on (SF) Imp and (SF) Hoare Logic! This will be a great improvement, especially for those who use SF to learn Rocq.

Here is a preview of those features. Any suggestions, comments, or stars on GitHub would mean a lot!