inria-00001173, version 4

Coq in a Hurry

Yves Bertot () ¹

3ème cycle (2010) 42 pages

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

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

Bibliographic reference

• Type of document: Lessons
• title: Coq in a Hurry
• abstract: 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.
• subject: Computer Science/Logic in Computer Science
• Level: 3eme cycle
• Date: 2010-05-26
• Place: Types Summer School, also used at the University of Goteborg, Nice,
  Ecole Jeunes Chercheurs en Programmation,
  Universite de Nice
• Number of pages: 42
• Content: 1 Expressions and logical formulas
  2 Programming in Coq
  3 Propositions and proofs
  4 Proving properties of programs on numbers
  5 Proving properties of programs on lists
  6 Defining new datatypes
  7 Numbers in the Coq system
  8 Inductive Properties
  9 Exercises
  10 Solutions

Attached file list to this document: 

• inria-00001173, version 4
• http://cel.archives-ouvertes.fr/inria-00001173
• oai:cel.archives-ouvertes.fr:inria-00001173
• From: Yves Bertot <>
• Submitted on: Tuesday, 23 February 2010 12:15:39
• Updated on: Wednesday, 24 February 2010 11:48:48