The Coq mailing list

[Benjamin Pierce <bcpierce AT cis.upenn.edu>]

The CoqArt book (Bertot and Casteran) has been very helpful for me.

   - Benjamin


On Sep 24, 2007, at 7:11 AM, Wan Hai wrote:

> 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
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club