<p>I'm not sure which properties you're after, but what about the original paper:</p>

<p>Thierry Coquand, Gérard P. Huet: The Calculus of Constructions. Inf. Comput. 76(2/3): 95-120 (1988)</p>

<p>I got it from: <a href="http://www.sciencedirect.com/science/article/pii/0890540188900053#" rel="nofollow">http://www.sciencedirect.com/science/article/pii/0890540188900053#</a></p>

CC BY-SA 3.0
2014-03-31T07:44:06.873Z
He is asking about the Calculus of Inductive Constructions, not the plain Calculus of Constructions. The former is an extension of the latter. A good reference may be this:
Th. Coquand and C. Paulin-Mohring. Inductively defined types. In P. Martin-Löf and G. Mints, editors, Proceedings of Colog’88, volume 417 of Lecture Notes in Computer Science. Sprin­ger-Verlag, 1990.
Jan Johannsen
CC BY-SA 3.0
2014-03-31T12:36:45.667Z
@JanJohannsen The problem with it is that it isn't freely available.
Konstantin Solomatov
CC BY-SA 3.0
2014-04-01T09:26:04.410Z
Thanks for the correction, Jan - btw parts of the paper are available on [Google books](http://books.google.at/books?id=o_f4UwiZtL0C)
lambda.xy.x
CC BY-SA 4.0
2019-08-26T07:55:40.523Z
@KonstantinSolomatov, did you end up finding "Inductively defined types" online? If you hit this problem, you can often ask for a draft from one of the authors.
Steven Shaw
CC BY-SA 3.0
2014-03-31T07:38:28.370Z
2014-03-31T07:38:28.370Z
lambda.xy.x
<p>You can try the Coq user manual, in particular <a href="https://coq.inria.fr/doc/language/cic.html" rel="nofollow noreferrer">this section</a> is pretty nice (the server seems to be down at the moment though).</p>

<p>For meta-theory you can try some recent work of Benjamin Werner <em>et al.</em>, see <a href="http://www.lmcs-online.org/ojs/viewarticle.php?id=675" rel="nofollow noreferrer">Proof-irrelevant model of CC with predicative induction and judgmental equality
</a> and <a href="http://arxiv.org/abs/0808.3928" rel="nofollow noreferrer">On the strength of proof-irrelevant type theories</a> for the most salient work.</p>

CC BY-SA 4.0
2014-04-01T21:49:29.707Z
2019-08-26T08:40:21.333Z
2019-08-26T08:40:21.333Z
cody
<p>I want to learn more about Calculus of Inductive Constructions. What can you recommend to read on this topic? All the materials which I found are either in French or too basic (the Coq'Art book).</p>

<p>The thing I am interested the most are not definitions but the proofs of important properties.</p>

<lo.logic><dependent-type>
Good description of Calculus of Inductive Construction
Konstantin Solomatov
# Good description of Calculus of Inductive Construction

(Asked by: username_0 on 2014-03-30)

I want to learn more about Calculus of Inductive Constructions. What can you recommend to read on this topic? All the materials which I found are either in French or too basic (the Coq'Art book).

The thing I am interested the most are not definitions but the proofs of important properties.

**Tags:** lo.logic, dependent-type


---

## 2 answers

### Answer by username_1 on 2014-03-31. Score: 4 | Accepted answer

I'm not sure which properties you're after, but what about the original paper:

Thierry Coquand, Gérard P. Huet: The Calculus of Constructions. Inf. Comput. 76(2/3): 95-120 (1988)

I got it from: <http://www.sciencedirect.com/science/article/pii/0890540188900053#>

> **Comments:**
> **username_2**: He is asking about the Calculus of Inductive Constructions, not the plain Calculus of Constructions. The former is an extension of the latter. A good reference may be this: Th. Coquand and C. Paulin-Mohring. Inductively defined types. In P. Martin-Löf and G. Mints, editors, Proceedings of Colog’88, volume 417 of Lecture Notes in Computer Science. Sprin­ger-Verlag, 1990.  
> **username_0**: @JanJohannsen The problem with it is that it isn't freely available.  
> **username_1**: Thanks for the correction, Jan - btw parts of the paper are available on [Google books](http://books.google.at/books?id=o_f4UwiZtL0C)  
> **username_3**: @KonstantinSolomatov, did you end up finding "Inductively defined types" online? If you hit this problem, you can often ask for a draft from one of the authors.  

---

### Answer by username_4 on 2014-04-01. Score: 6

You can try the Coq user manual, in particular [this section](https://coq.inria.fr/doc/language/cic.html) is pretty nice (the server seems to be down at the moment though).

For meta-theory you can try some recent work of Benjamin Werner *et al.*, see [Proof-irrelevant model of CC with predicative induction and judgmental equality](http://www.lmcs-online.org/ojs/viewarticle.php?id=675) and [On the strength of proof-irrelevant type theories](http://arxiv.org/abs/0808.3928) for the most salient work.


---

