inria-00001173, version 5

Coq in a Hurry

Yves Bertot () ¹

3ème cycle (2010) 43 pages

• 1 :  MARELLE (INRIA Sophia Antipolis)
• http://www-sop.inria.fr/marelle/
  INRIA France

Versions disponibles :  v1 (29-03-2006) v2 (24-05-2006) v3 (07-11-2008) v4 (24-02-2010) v5 (10-05-2010)

Références bibliographiques

• Type de publication : Cours
• Titre : Coq in a Hurry
• Résumé : 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.
• Domaine : Informatique/Logique en informatique
• Niveau du cours : 3ème cycle
• Date du cours : 26/05/2010
• Lieu du cours : Types Summer School, also used at the University of Goteborg, Nice,
  Ecole Jeunes Chercheurs en Programmation,
  Universite de Nice
• Nombre de pages : 43
• Tables des matières : Expressions and logical formulas
  Programming in Coq
  Propositions and proofs
  Proving properties of programs on numbers
  Proving properties of programs on lists
  Defining new datatypes
  Numbers in the Coq system
  Inductive properties
  

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