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

<p>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 <a href="http://en.wikipedia.org/wiki/Automath" rel="noreferrer">Automath</a> system.</p>

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

<p>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 <a href="http://www.mpi-sws.org/~skilpat/plerg/papers/martin-lof-meanings-2up.pdf" rel="noreferrer">On the Meaning of the Logical Constants and the Justification of Logical Laws</a>. He reasons that both in logic and mathematics, the meaning of constructions can be given by examining the <strong>introduction rules</strong> which allow the formation of those constructions as judgements, e.g. for conjunction
$$ \frac{\vdash A\quad \vdash B}{\vdash A\wedge B}$$</p>

<p>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" <strong>predicative universes</strong>, 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).</p>

<p>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 <strong>inductively defined families</strong>. 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 <strong>ITT</strong>.</p>

<p>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 <strong>Calculus of Constructions (CoC)</strong>, 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 <a href="https://coq.inria.fr/" rel="noreferrer">Coq</a> system we know and love.</p>

<p>I highly suggest <a href="http://www.sciencedirect.com/science/article/pii/0890540188900053#" rel="noreferrer">this</a> 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 <a href="http://plato.stanford.edu/entries/type-theory/" rel="noreferrer">article</a> on type theory, though it doesn't explain the C-H correspondence in much detail.</p>

CC BY-SA 3.0
2015-03-02T21:57:35.163Z
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.
Martin Berger
CC BY-SA 3.0
2015-03-02T23:31:03.100Z
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
CC BY-SA 3.0
2015-03-02T23:31:39.750Z
Inductive types were added to improve the *computational* behavior in addition to this.
cody
CC BY-SA 3.0
2015-03-03T08:24:03.293Z
In what sense do inductive types improve computational behaviour?
Martin Berger
CC BY-SA 3.0
2015-03-03T14:15:35.233Z
Well, the predecessor function can not be computed in constant time using the impredicative definition for natural numbers. See e.g. [here](http://link.springer.com/chapter/10.1007%2F3-540-52753-2_47) or [here](http://repository.cmu.edu/cgi/viewcontent.cgi?article=2907&context=compsci).
cody
CC BY-SA 3.0
2015-03-16T18:29:47.893Z
Thanks, but constant time in what sense? Church numberals? If you implement
numbers as bit strings then predecessor is not constant time
on Turing machines either.
Martin Berger
CC BY-SA 3.0
2015-03-16T19:45:57.480Z
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
CC BY-SA 3.0
2016-07-08T13:23:44.693Z
I'm trying to get my head around type theory. I'm wondering, given CoC is better than M-L's ITT, is it necessary to go back to understand M-L's work at all? i.e. can I get a good grasp of type theory by understanding merely CoC? Where does UTT fit into this? Idris uses something like UTT and I think Agda does too.
Steven Shaw
CC BY-SA 3.0
2016-07-08T14:33:10.983Z
@StevenShaw Maybe my answer gave the wrong impression, but CoC isn't "better" than ML type theory, except maybe in some philosophical aspects, but that's very debatable. Coq integrates many aspects of both, and I think getting a good understanding of type theory will requires several sources, possibly starting with those referenced here: http://cstheory.stackexchange.com/questions/6136/what-is-the-most-intuitive-dependent-type-theory-i-could-learn.
cody
CC BY-SA 3.0
2016-07-08T14:34:07.817Z
The only UTT i've ever heard of is *Unintentional Type Theory*: https://ncatlab.org/nlab/show/unintentional+type+theory but I don't think that's what you meant :)
cody
CC BY-SA 3.0
2016-07-08T16:35:35.737Z
Thanks for answering! I'm glad I asked otherwise I would have gotten the idea that CoC was better than M-L's ITT. I have roughly followed all the advice given in the answer you mention -- but I could do much better at understanding it all :). UTT is Luo's UTT. I'm pretty sure it stands for Unified Type Theory. The reference is always his book "Computation and Reasoning". I've been wondering whether to buy that one...
Steven Shaw
CC BY-SA 3.0
2016-07-08T18:26:42.300Z
In that case, I'd probably recommend "The Metatheory of UTT" by H. Goguen. I think any of these references will assume knowledge of basic type theory though, say at the level of Pierce's "Types and Programing Languages".
cody
CC BY-SA 3.0
2016-07-13T07:55:03.713Z
@MartinBerger can you expand or give a pointer on "you cannot prove induction in CoC"?
phadej
CC BY-SA 3.0
2016-07-13T09:48:30.463Z
@phadej Not sure where this is explained best, it's been a while since I looked at this. Maybe [Inductively defined types in the Calculus of
Constructions](http://repository.cmu.edu/cgi/viewcontent.cgi?article=2907&context=compsci) by F. Pfenning and C. Paulin-Mohring is a good start?
Martin Berger
CC BY-SA 3.0
2018-01-15T04:58:35.653Z
@Joel Burget is "Unfortunately" really ambiguous? It means unfortunately for that theory. I think it clarifies.
Caleb Stanford
CC BY-SA 3.0
2015-03-02T20:36:54.807Z
2018-01-14T18:23:00.517Z
2018-01-14T18:23:00.517Z
cody
<p>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.</p>

CC BY-SA 3.0
2011-08-01T15:54:20.067Z
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
CC BY-SA 3.0
2011-08-01T16:00:00.590Z
Ah and a good discussion of some of these things can be found in Geuvers : http://www.cs.ru.nl/~herman/PUBS/CC_CHiso.ps.gz
cody
CC BY-SA 3.0
2011-08-02T08:56:34.363Z
Thanks for the comments and linked paper, cody. It looks what I am seeking for.
day
CC BY-SA 3.0
2016-07-08T11:51:15.240Z
A pdf version of the paper mentioned by @cody: http://www.cs.ru.nl/~herman/PUBS/CC_CHiso.pdf
Steven Shaw
<type-theory>
What's the relation and difference between Calculus of Inductive Constructions and Intuitionistic Type Theory?
day
# What's the relation and difference between Calculus of Inductive Constructions and Intuitionistic Type Theory?

(Asked by: username_0 on 2011-07-30)

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.

**Tags:** type-theory

> **Comments:**
> **username_1**: 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.  
> **username_1**: Ah and a good discussion of some of these things can be found in Geuvers : http://www.cs.ru.nl/~herman/PUBS/CC_CHiso.ps.gz  
> **username_0**: Thanks for the comments and linked paper, username_1. It looks what I am seeking for.  
> **username_2**: A pdf version of the paper mentioned by @username_1: http://www.cs.ru.nl/~herman/PUBS/CC_CHiso.pdf  

---

## 1 answers

### Answer by username_1 on 2015-03-02. Score: 29

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](http://en.wikipedia.org/wiki/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](http://www.mpi-sws.org/~skilpat/plerg/papers/martin-lof-meanings-2up.pdf). 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](https://coq.inria.fr/) system we know and love.

I highly suggest [this](http://www.sciencedirect.com/science/article/pii/0890540188900053#) 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](http://plato.stanford.edu/entries/type-theory/) on type theory, though it doesn't explain the C-H correspondence in much detail.

> **Comments:**
> **username_3**: 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.  
> **username_1**: Yes, I forgot to comment on this. However, adding the simple axiom $1\neq 0$ suffices (for a suitable encoding of the concepts involved).  
> **username_1**: Inductive types were added to improve the *computational* behavior in addition to this.  
> **username_3**: In what sense do inductive types improve computational behaviour?  
> **username_1**: Well, the predecessor function can not be computed in constant time using the impredicative definition for natural numbers. See e.g. [here](http://link.springer.com/chapter/10.1007%2F3-540-52753-2_47) or [here](http://repository.cmu.edu/cgi/viewcontent.cgi?article=2907&context=compsci).  
> **username_3**: Thanks, but constant time in what sense? Church numberals? If you implement numbers as bit strings then predecessor is not constant time on Turing machines either.  
> **username_1**: 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! :)  
> **username_2**: I'm trying to get my head around type theory. I'm wondering, given CoC is better than M-L's ITT, is it necessary to go back to understand M-L's work at all? i.e. can I get a good grasp of type theory by understanding merely CoC? Where does UTT fit into this? Idris uses something like UTT and I think Agda does too.  
> **username_1**: @StevenShaw Maybe my answer gave the wrong impression, but CoC isn't "better" than ML type theory, except maybe in some philosophical aspects, but that's very debatable. Coq integrates many aspects of both, and I think getting a good understanding of type theory will requires several sources, possibly starting with those referenced here: http://cstheory.stackexchange.com/questions/6136/what-is-the-most-intuitive-dependent-type-theory-i-could-learn.  
> **username_1**: The only UTT i've ever heard of is *Unintentional Type Theory*: https://ncatlab.org/nlab/show/unintentional+type+theory but I don't think that's what you meant :)  
> **username_2**: Thanks for answering! I'm glad I asked otherwise I would have gotten the idea that CoC was better than M-L's ITT. I have roughly followed all the advice given in the answer you mention -- but I could do much better at understanding it all :). UTT is Luo's UTT. I'm pretty sure it stands for Unified Type Theory. The reference is always his book "Computation and Reasoning". I've been wondering whether to buy that one...  
> **username_1**: In that case, I'd probably recommend "The Metatheory of UTT" by H. Goguen. I think any of these references will assume knowledge of basic type theory though, say at the level of Pierce's "Types and Programing Languages".  
> **username_4**: @MartinBerger can you expand or give a pointer on "you cannot prove induction in CoC"?  
> **username_3**: @username_4 Not sure where this is explained best, it's been a while since I looked at this. Maybe [Inductively defined types in the Calculus of Constructions](http://repository.cmu.edu/cgi/viewcontent.cgi?article=2907&context=compsci) by F. Pfenning and C. Paulin-Mohring is a good start?  
> **username_5**: @Joel Burget is "Unfortunately" really ambiguous? It means unfortunately for that theory. I think it clarifies.  

---

