Ce cours est maintenant assuré par Hugo Herbelin. Les documents ci-dessous concernent l'ancienne version du cours

Notes de cours (préparées par Alexandre Miquel):

• Le document principal
• Le système T de Gödel
• Un petit guide de survie pour Coq

Quelques notes pour le cours 1.

L'encodage Coq de la déduction naturelle présenté en cours : NatDed.

Annales d'examen : sujet de mai 2015.

Projet 2019-2020 : le dépot git à forker. Plus d'information dans le README.

Sujets des TD/TP:

• TD1 (déduction naturelle): pdf
• TD2 (premiers pas en Coq): markdown
• TD3 (arithmétique de Peano): pdf
• TD4 (maths élémentaires en Coq): markdown
• TD5 (entiers naturels en Coq): markdown
• TD6 (listes en Coq): markdown
• TD7 (théories et modèles): pdf
• TD8 (prédicats inductifs): markdown
• TD9 (énigme de MU): markdown
• TD9bis (damier): markdown
• TD10 (système T et théorie des types simples): pdf