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.


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#

| cite | improve this answer | |
  • 7
    $\begingroup$ 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. $\endgroup$ – Jan Johannsen Mar 31 '14 at 7:44
  • $\begingroup$ @JanJohannsen The problem with it is that it isn't freely available. $\endgroup$ – Konstantin Solomatov Mar 31 '14 at 12:36
  • 1
    $\begingroup$ Thanks for the correction, Jan - btw parts of the paper are available on Google books $\endgroup$ – lambda.xy.x Apr 1 '14 at 9:26
  • $\begingroup$ @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. $\endgroup$ – Steven Shaw Aug 26 '19 at 7:55

You can try the Coq user manual, in particular this section 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 and On the strength of proof-irrelevant type theories for the most salient work.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.