 |
 |
 |
|
|
|
| HAL : inria-00001173, version 5 |
| Fiche détaillée |  Récupérer au format |
 |
| 3ème cycle (2010) 43 pages |
|
|
| Versions disponibles : | v1 (29-03-2006) | v2 (24-05-2006) | v3 (07-11-2008) | v4 (24-02-2010) | v5 (10-05-2010) |
|
|
|
|
| Coq in a Hurry |
|
|
| Yves Bertot 1 |
|
|
| (26/05/2010) |
|
|
|
| These notes provide a quick introduction to the Coq system and show how it can be used to define logical concepts and functions and reason about them. It is designed as a tutorial, so that readers can quickly start their own experiments, learning only a few of the capabilities of the system. A much more comprehensive study is provided in [1], which also provides an extensive collection of exercises to train on. |
|
|
|
|
|
|
|
|
|
|
|
| 1 : | MARELLE (INRIA Sophia Antipolis) |
|
|
|
INRIA |
|
|
|
|
|
|
|
|
|
| Domaine | : | Informatique/Logique en informatique |
|
|
| Liste des fichiers attachés à ce document : | ||||||||||
|
||||||||||
|
|
|
| inria-00001173, version 5 | |
| http://cel.archives-ouvertes.fr/inria-00001173 | |
| oai:cel.archives-ouvertes.fr:inria-00001173 | |
| Contributeur : Yves Bertot | |
| Soumis le : Vendredi 23 Avril 2010, 10:05:32 | |
| Dernière modification le : Lundi 10 Mai 2010, 16:22:33 | |
