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

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.

• To me ITT means "Intuitionnistic Type Theory" which could mean a number of things. In particular there are a large number of subtle variations from the original Martin-Lof description(s!), and it would help discussion if you gave the reference which describes the ITT you are thinking of. The short answer is this: ITT in the Martin-Lof sense without universe is a sub-theory of the CoC. In the presence of universes but no inductive types, you can crush all the universes into the single impredicative universe of the CoC. With large inductive types and large elimination, things are more complex.
– cody
Aug 1, 2011 at 15:54
• Ah and a good discussion of some of these things can be found in Geuvers : cs.ru.nl/~herman/PUBS/CC_CHiso.ps.gz
– cody
Aug 1, 2011 at 16:00
• Thanks for the comments and linked paper, cody. It looks what I am seeking for.
– day
Aug 2, 2011 at 8:56
• A pdf version of the paper mentioned by @cody: cs.ru.nl/~herman/PUBS/CC_CHiso.pdf Jul 8, 2016 at 11:51

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.

• It might be worth remarking that the CoC, for all the power of its impredivative construction of data types, cannot prove induction, and later authors (e.g. Paulin-Mohring) extended the CoC with with inductive constructions a la Martin-Löf, yielding the Calculus of Inductive Constructions, which is used in Coq. Mar 2, 2015 at 21:57
• Yes, I forgot to comment on this. However, adding the simple axiom $1\neq 0$ suffices (for a suitable encoding of the concepts involved).
– cody
Mar 2, 2015 at 23:31
• Inductive types were added to improve the computational behavior in addition to this.
– cody
Mar 2, 2015 at 23:31
• Well, the predecessor function can not be computed in constant time using the impredicative definition for natural numbers. See e.g. here or here.
– cody
Mar 3, 2015 at 14:15
• Yes, Church numerals, but a similar result is going to hold for more sensible data-types like linked lists. The Turing Machine example tends to suggest that Turing Machines are not well-suited for practical computation either! :)
– cody
Mar 16, 2015 at 19:45