5
$\begingroup$

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.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
4
$\begingroup$

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#

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

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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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