Commentary by cpressey on Coq works
Software Foundations
So this is actually a collection of several volumes. Should I split it up? Not sure.
As of 2024 the first volume is at version 6.6. I don't know when this started.
Certified Programming with Dependent Types
I haven't read it yet, but this is an open-access book about Coq.
Modeling and Proving in Computational Type Theory Using the Coq Proof Assistant (Draft)
One thing that strikes me is that the authors say they're working in a "computational type theory", but AFAICT it is not what has been labelled "Computational Type Theory" in the literature (by e.g. Constable). (Which is fine because I'm a bit suspicious of Constable's CTT anyway.)
Again AFAICT it doesn't look like they're implementing their own type theory in Coq, so it's probably that their type theory can be expressed as a subset of CIC, and they are just working in Coq directly.
Recursive Datatypes and Inductive Proofs
Interactive Theorem Proving with Coq
Pragmatic Quotient Types in Coq
It has more detail than I need on the implementation and how the implementation fits into how Coq sees the world (that's the "pragmatic" part I suppose) but the explanation of quotienting in the intro, it's worth reading just for that.
Interaction Trees
I thought this was very intruiging. The ITree described in the paper is basically the so-called "freer monad". They add a "Tau" to it to make it compatible with Coq (where all expressions must terminate). This might be (I'm not sure) seen as combining it with the "delay monad". But Tau is also weirdly reminiscent of "stuttering" in TLA+, but that might be a coincidence. Anyway it plays nicely with Coq and can be used in bisimulation proofs.
The "MonadIter" iteration monad works on something like
data MonadIter a b = Run a
| Stop b
A function iter takes a function and runs it until it returns Stop.
Also - many of the equations presented in the paper seem surprisingly equational, too. But I don't know what I mean by that.
Standard Library | The Coq Proof Assistant
implication - Transitivity of -> in Coq - Stack Overflow
proof - Proving (\~A -> \~B)-> (\~A -> B) -> A in Coq - Stack Overflow
coq - Proving f (f bool) = bool - Stack Overflow
DProp.Prop
Implementing a deep embedding of Propositional Logic in Coq, and going through what it all means.