coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
Archive powered by MhonArc 2.6.16.