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

Enseignant : Adam Chlipala

Page perso : http://www.cs.berkeley.edu/~adamc/

Documents référencés

Pour voir les documents d’une ressource écrits par d’autres enseignants, cliquez sur son titre, ou bien sur son icône ou .

Interactive Computer Theorem Proving

Thème : Logique & Preuve – Cursus : Berkeley

2006 - 2007

Cours

Open Office sources on the web page.

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

Accueil Plan du site Contact et proposition de documents : qravs-ng-yvfgrf-qbg-raf-ylba-qbg-se

Les documents référencés sur ce site sont la propriété intellectuelle de leurs auteurs respectifs. Ne pas les reproduire sans autorisation.

Le code source de ce site est placé sous licence GPLv3.