What's the relation and difference between Calculus of Inductive Constructions and Intuitionistic Type Theory?

Question

As stated in the title, I wonder any relation and difference between CIC and ITT. Could someone explain or point to me some literature that compares these two systems? Thanks.

Answer 1

I've already answered somewhat, but I'll try to give a more detailed overview of the type theoretical horizon, if you will.

I'm a bit fuzzy on the historical specifics, so more informed readers will have to forgive me (and correct me!). The basic story is that Curry had uncovered the basic correspondence between simply-typed combinators (or $\lambda$-terms) and propositional logic, which was extended by Howard to cover first-order logic, and IIRC independently discovered by de Bruijn in investigations around the hugely influential Automath system.

The Automath system was a refinement of Church's simple type theory which itself was a dramatic simplification of Russel and Whitehead's type theory with universes and the axiom of reducibility. This was relatively well-known logical terrain by the 1960s.

However, giving a coherent, simple, foundational system that encompassed both proof and term systems was still a very open question by 1970, and a first answer was given by Per Martin-Löf. He gives a very philosophical overview On the Meaning of the Logical Constants and the Justification of Logical Laws. He reasons that both in logic and mathematics, the meaning of constructions can be given by examining the introduction rules which allow the formation of those constructions as judgements, e.g. for conjunction $$ \frac{\vdash A\quad \vdash B}{\vdash A\wedge B}$$

Determines the corresponding elimination rule. He then gave a very powerful foundational system based on such judgements, allowing him to give a foundational system similar to Automath using very few syntactic constructions. Girard found that this system was contradictory, prompting Martin-Löf to adopt "Russel-style" predicative universes, severely limiting the expressiveness of the theory (by effectively removing the axiom of reducibility) and making it slightly more complex (but had the advantage of making it consistent).

The elegant constructions allowing for the definition of the logical symbols didn't work anymore though, which prompted M-L to introduce them in a different form, as inductively defined families. This is a very powerful idea, as it allows defining everything from judgmental equality and logical operators to natural numbers and functional data-types as they appear in computer science. Note that each family we add is akin to adding a number of axioms, which need to be justified as consistent in each instance. This system (dependent types + universes + inductive families) is usually what is referred to as ITT.

However there was some lingering frustration, as the powerful but simple foundational system was inconsistent, and the resulting system was more complex, and somewhat weak (in the sense that it was difficult to develop much of the modern mathematical framework in it). Enter Thierry Coquand, who with his supervisor Gerard Huet, introduced the Calculus of Constructions (CoC), which mostly solved these issues: a unified approach to proofs and data-types, a powerful (impredicative) foundational system and the ability to define "constructions" of the logical or mathematical variety. This eventually matured into an actual implementation of a system designed as a modern alternative to Automath, culminating in the Coq system we know and love.

I highly suggest this foundational paper on CoC, as Thierry knows a ridiculous amount about the historical development of type theory, and probably explains this much better than I. You might also want to check out his article on type theory, though it doesn't explain the C-H correspondence in much detail.