The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Hi all,

This message is to announce a new version of a document called "Coq in 
Hurry", designed as a short tutorial to the Coq system, aiming at a 
public whose main background would be programming (but not necessarily 
functional programming).  The objective is to describe a 
"self-contained" subset of the Coq facilities, strong enough to let 
people write programs and prove their correctness and to give a 
practical feeling while avoiding theoretical issues.

This is available at the following address

http://cel.archives-ouvertes.fr/inria-00001173/

My own usage of these notes it to provide the Coq training that is 
enough for a course in programming language semantics where all concepts 
are then encoded and reasoned about in the Coq system.

I will be happy to receive feedback on this tutorial, especially on the 
following matters:

- How long would it take to a real beginner to read through the notes 
and make the exercises?
- What is really the necessary background?  I hope to provide material 
that can be understood by people who start  with just a basic training 
in programming with a conventional programming language (C or Java), is 
that reasonable?

Yves