coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to study "Calculus of Inductive Constructions"

From: "Wan Hai" <wan.whyhigh AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] How to study "Calculus of Inductive Constructions"
Date: Mon, 24 Sep 2007 19:11:43 +0800
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:mime-version:content-type:content-transfer-encoding:content-disposition; b=QPtAxd5KScYXCL5IUoe/DzHxf+xVIdl+BIC68C5aftex+JUS8XyPYo8WMVnfZ/le5JyNK8bAClQEYIkR2s00hyhW1+mIVXqs4RRM1Zhr/vChq6SkFuag9TiCweLfFdxSFdU8kqVribcPjRHfOF3yhTlNJ2kQ/XKczOvKPvGGJbw=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi All,

I was a PVS user before, now I turn to Coq. As an beginner, I have
some questions to ask. May someone kindly give answers for me?

1) If I want to use Coq efficiently, need I study the "Calculus of
Inductive Constructions"?
2) Is the information provided in chapter 4 of "The Coq Proof
Assistant Reference Manual" enough? 4.1-4.5.1 are not difficult for me
to understand. But from 4.5.2 on, I found it is difficult. Is there
some preknowledge of chapter 4 I need to read first?
3) If I want to learn "Calculus of Inductive Constructions" better,
what books or papers you suggest me to read?

Thanks a lot!

Wan Hai
20070924

[Coq-Club] How to study "Calculus of Inductive Constructions", Wan Hai
- Re: [Coq-Club] How to study "Calculus of Inductive Constructions", Benjamin Pierce
- [Coq-Club] Confused about the "move" tactic, Wei Hu
  - Re: [Coq-Club] Confused about the "move" tactic, Hugo Herbelin