DENIF – Documents d’Enseignement Numériques en Informatique Fondamentale

   Cours  

•   Lecture 1 : Introduction
•   Lecture 2 : Basic logic and natural deduction
•   Lecture 3 : Data structures and induction
•   Lecture 4 : Inductively-defined predicates
•   Lecture 5 : Proofs as programs (missing)
•   Lecture 6 : Tactics for automation
•   Lecture 7 : Programming with proofs
•   Lecture 8 : Easier programming with proofs (no slides)
•   Lecture 9 : Beyond primitive recursion
•   Lecture 10 : More fun with automation (no slides)
•   Lecture 11 : Proof by reflection
•   Lecture 12 : Denotational semantics (no slides)
•   Lecture 13 : Reflecting Coq into Coq (no slides)
•   Lecture 14 : Twelf

   Complements  

•   Homework and solutions, source codes, html docs