> Coq is the result of more than 20 years of research. It started in 1984 from an implementation of the Calculus of Constructions at INRIA-Rocquencourt by Thierry Coquand and Gérard Huet. In 1991, Christine Paulin extended it to the Calculus of Inductive Constructions.
The CoC provides the basic framework for Coq, while the Co(I)C or even the Calculus of (Co)-Inductive Constructions provides a dramatic extension in power and expressivity necessary for "real" programming in Coq.
> It's also, IIRC, based on a logical model called the Calculus of Constructions
"Calculus of Inductive Constructions" (https://coq.inria.fr/about-coq)
From your link:
> Coq is the result of more than 20 years of research. It started in 1984 from an implementation of the Calculus of Constructions at INRIA-Rocquencourt by Thierry Coquand and Gérard Huet. In 1991, Christine Paulin extended it to the Calculus of Inductive Constructions.
The CoC provides the basic framework for Coq, while the Co(I)C or even the Calculus of (Co)-Inductive Constructions provides a dramatic extension in power and expressivity necessary for "real" programming in Coq.