Accueil
Connexion
DENIF –
Documents d’Enseignement Numériques en Informatique Fondamentale
Thèmes
Cursus
Enseignants
Interactive Computer Theorem Proving
Thème :
Logique & Preuve
–
Cursus :
Berkeley
2006 - 2007
Cours
Open Office sources on the web page.
Adam Chlipala
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