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):

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