Enseignements

Année 2012-2013

Preuves sur ordinateur

Je donne au premier semestre les TD/TP pour le cours de Preuves sur ordinateur donné par Colin Riba.
  1. λ-calcul et codage des types de données (sujet.pdf et corrigé.pdf)
  2. Réduction du sujet, correspondance de Curry-Howard et théorème de Glivenko (sujet.pdf)
    Pour le DM, si vous prenez la réduction du sujet, voici un modele.tex et le corrigé.pdf. Le corrigé du théorème de Glivenko en Coq.
  3. Reprise de Curry-Howard et induction dans HA (sujet.v ou sujet.html et corrigé.v)
  4. Tactiques automatiques et division entière (sujet.v ou sujet.html et corrigé.v))
    Voici le sujet du second DM, vous devez démontrer les propositions de la partie 2.
  5. Filtrage dépendant (sujet.v ou sujet.html et corrigé.v)
  6. Le prédicat d'accessiblité Acc (sujet.v ou sujet.html et corrigé.v)
    Un premier morceau du DM à venir la semaine prochaine. Regardez-le pour me poser des questions jeudi 25 octobre.
  7. Codages de types de données dans système F (sujet.pdf et corrigé.pdf)
    Voici également les DM 3 et 4:
  8. IPP et preuves par réflection (sujet.v ou sujet.html)
  9. Calcul des séquents (sujet.pdf et corrigé.pdf)
  10. Réversibilités dans LK₀ (sujet.pdf et corrigé.pdf)
  11. Théorème de Herbrand (sujet.pdf et corrigé.pdf)
    Voici enfin le modèle pour le dernier DM: le modèle Herbrand.v (avec quelques corrections)
    ainsi que le fichier OptBool.vo (versions pour Coq 8.2, Coq 8.3 pour SLS, Coq 8.3 pour Ubuntu et Coq 8.4, les enregistrer sous le nom « OptBool.vo »).
    Pour éviter de devoir encore mutiplier les binaires (et pour le plus grand plaisir de Rémi), voici le fichier source correspondant OptBool.v.
  12. Résolution (sujet.pdf et corrigé.pdf)

Introduction à l'Informatique

Je donne également au premier semestre les TP pour le cours d'Introduction à l'Informatique donné par Stephan Thomasse dans le cadre du master Systèmes Complexes.
  1. Connexité des graphes aléatoires (corrigé)
  2. Arbres couvrants (corrigé)
  3. Calcul de plus courts chemins dans un graphe (corrigé)
  4. Tris (corrigé)
  5. Automates et recherche dans un texte (corrigé)

Introduction à l'informatique théorique

Toujours au premier semestre, je donne les cours/TD/TP pour le cours Introduction à l'informatique théorique de la classe passerelle avec Guillaume Hanrot.

Initiation réseaux et base de données

Enfin, je donne des TP dans le cours d'Initiation réseaux et base de données donné par Fabien Duchateau à l'UCBL.