Logique : INF 462

Transparents en pdf et en anglais (Yves Bertot, Pierre Castéran)

Cours donné à L'université de Tsinghua en Aout 2009

Exercices

Mode d'emploi des exercices : télécharger les fichiers en gardant l'extension .v; ils contiennent toutes les déclarations nécessaires. Les textes des exercices sont dans les commentaires.



Note : Il y aura toujours plus d'exercices que ce qu'on peut faire normalement en une séance de TD. Les solutions seront publiées le mercredi au plus tard, et pourront être discutées le TD suivant.
Il y a deux outils pour travailler en Coq.
Pour les habitués d'Emacs : utiliser Proof General (voir note en bas de page), qui est un mode Emacs spécialisé dans les preuves interactives.

Ceux qui préfèrent les "ide" , utiliser coqide, l'environnement de développement intégré pour Coq.
coqide est moins usine à gaz qu'Eclipse. Si un bug provoqué par la diabolique touche MOD4 (celle avec une fenêtre tordue) de votre clavier se produit, alors éditer votre fichier $HOME/.coqiderc et remplacer toutes les occurrences de MOD4 par MOD1, puis relancer.


Projet

L'énoncé à télécharger
Foire aux questions
Un corrige possible

Préparation à l'examen

Liens et informations utiles