Ce cours est une introduction pratique au calcul des constructions et à son utilisation pour vérifier des preuves sur ordinateur. Ce cours est décomposé en deux séances (3 heures chacune).
La première séance décrit le codage de la logique dans le calcul des constructions pures et montre l'utilisation des tactiques les plus simples. Les transparents sont disponibles en postscript compressé (gzip).
La deuxième séance décrit les raisonnements par récurrence et leur codage dans le calcul des constructions inductives. postscript compressé (gzip).
Nous fournissons aussi un fichier compressé au format zip, qui contient les deux cours.