Some resources about Coq

Teaching related to Coq

• Guest Lecture (UNSW Sydney, 2004)
  • An introductory lecture: Overview of the Coq Proof Assistant
  • some demos (or_commute.v, tree.v, coins.v, mod2.v, dep.v)

• Cours Ingéniérie de la preuve / Certification du Logiciel (Université de Strasbourg)

• Useful links: Coq homepage, exercices from Coq'Art

Changing Data Representation

• CDR: a tool designed to make changing data representation easier in a type-theory based proof assistant like Coq

Programming Styles

• Programming x^n efficiently in Coq - plain recursive, iterative (tail-recursive) and cps-style programs

Dependent Types

• Dependent lists (vectors): zip, unzip with dependent lists (upgraded from coq V7.2 to coq8.0)
  • definitions.v (v8), lemmas.v (v8), theorems.v (v8)

• Programming with Dependent Types in Coq: a Study of Square Matrices

Other Proofs

• An axiom leading to proof irrelevance (Proof_irrelevance.v)

  (forall A B : Prop, (A <-> B) -> A = B) -> forall (A : Prop) (p q : A), p = q
  

• Proof of Scott Theorem for fixpoint equations (Scott.v)

• Sujet de TP (M2ISI) : propriétés d'anneau des entiers de Gauss