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.

Calculus of Constructions

Introduction to the Calculus of Inductive Constructions

• rating: 1

Inductive types were added to the Calculus of Constructions, not because the CoC was incapable of expressing inductive types, but because doing so in the CoC alone is awkward and (when implemented) inefficient.

When giving axioms in first-order logic there is a risk that the theory has no model (everything can be proven). There is no such risk with inductive definitions. Syntactic conditions ensure the existence of a model. (In computational terms (mine) the reasoning chain about the induction is guaranteed to terminate.) It seems the strict-positivity conditions are a part of this.

Around page 8 it starts to lurch towards Coq instead of the CIC itself.

It also starts mentioning some things that sound like special cases, that make me think CIC is more of an "expedient" system than I had hoped; in particular, "There are exceptions where any elimination is allowed". It's reasonable, I suppose, if it makes the (human) theorem prover's life easier? To an extent.

The Calculus of Inductive Constructions

• rating: 1

This is good for a high-level view of how history has built up the Calculus of Constructions over time.

lo.logic - Intuitive explanation of the fact that the Calculus of Constructions is not conservative over Higher-Order Logic - Theoretical Computer Science Stack Exchange

• rating: 1

.

atennapel/coc-os: "operating system" based on the calculus of constructions

• rating: 1

Not actually Coq: Calculus of Constructions only. And more like a REPL than an OS I think!