Commentary by Chris Pressey

This work is distributed under a CC-BY-ND-4.0 license, with the following explicit exception: the ratings may be freely used for any purpose with no limitations.

Coq

Software Foundations

• rating: 3

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

• rating: TODO

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)

• rating: TODO

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

• rating: TODO

.

Interactive Theorem Proving with Coq

• rating: TODO

.

Pragmatic Quotient Types in Coq

• rating: 1

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

• rating: 2

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

• rating: 1

.

implication - Transitivity of -> in Coq - Stack Overflow

• rating: 1

.

proof - Proving (\~A -> \~B)-> (\~A -> B) -> A in Coq - Stack Overflow

• rating: 1

.

coq - Proving f (f bool) = bool - Stack Overflow

• rating: 1

.

DProp.Prop

• rating: 1

Implementing a deep embedding of Propositional Logic in Coq, and going through what it all means.

Address a \"setoid hell\"? · Issue #10871 · coq/coq

• rating: 1

.

coq - Defining Kripke models and the canonical model for $S4$ modal logic - Proof Assistants Stack Exchange

• rating: 1

.

JasonGross/coq-union-find: A repository for playing with union-find in Coq

• rating: 1

.

codyroux/tinymatch: A teeny language with nats, lists and pattern matching, static and dynamic semantics and a proof of progress and preservation.

• rating: 1

.

plclub/hs-to-coq: Convert Haskell source code to Coq source code.

• rating: 1

.

Ana de Almeida Borges / Coq formalization of QRC1 · GitLab

• rating: 0

.