 |
 |
 |
|
|
|
| HAL: inria-00001173, version 5 |
| Detailed view |  Export this paper |
 |
| 3ème cycle (2010) 43 pages |
|
|
| Available versions: | v1 (2006-03-29) | v2 (2006-05-24) | v3 (2008-11-07) | v4 (2010-02-24) | v5 (2010-05-10) |
|
|
|
|
| Coq in a Hurry |
|
|
| Yves Bertot 1 |
|
|
| (2010-05-26) |
|
|
|
| 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 |
|
|
|
|
|
|
|
|
|
| subject | : | Computer Science/Logic in Computer Science |
|
|
| Attached file list to this document: | ||||||||||
|
||||||||||
|
|
|
| inria-00001173, version 5 | |
| http://cel.archives-ouvertes.fr/inria-00001173 | |
| oai:cel.archives-ouvertes.fr:inria-00001173 | |
| From: Yves Bertot | |
| Submitted on: Friday, 23 April 2010 10:05:32 | |
| Updated on: Monday, 10 May 2010 16:22:33 | |
