The Coq mailing list

[Cody Roux <Cody.Roux AT loria.fr>]

On Tue, 2010-09-21 at 16:15 +0200, Gergely Buday wrote:
> Hi there,
> 
> do I understand correctly that the underlying logic of Coq is the
> extended calculus of constructions, as described in
> 
> http://www.cs.rhul.ac.uk/~zhaohui/THESIS90.ps ;?
> 
> Or, there were some new developments influencing the kernel code?
> 
> - Gergely

        The logic in Coq is essentially a combination of Luo's ECC and the
Calculus of Inductive Constructions. The extensions to ECC are
essentially:

* Large and Small Inductive and Coinductive types, with a strict
positivity condition.
* A fix-point operator that allows the definition of recursive
functions, with a guard condition that (hopefully) prohibits
non-terminating functions and thus guarantees the consistency of the
system, and an analogous cofix-point operator.
* Separation of Type0 into Prop and Set, with Prop Impredicative. Large
eliminations are forbidden on Prop, and it is forbidden to eliminate
from an element of kind Prop to one of kind Set (as it would render the
above restriction useless).

This is the big picture, and there are a few hacks in the theory that
allow it to be more friendly for certain applications (like allowing the
elements of Acc to be eliminated to an element of Set kind). I believe
that each aspect of this theory is discussed somewhere, but AFAIK there
is no self-contained global description of the theory along with proofs
of meta-theoretical properties. Of course the system is described in the
user manual.

Hope this helps.

Cody