Preuves Assistées par Ordinateur (Master 1) 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