LT INFO4

Consignes pour installer l'environnement de travail
Consignes générales pour les travaux à rendre sur chamilo
Remarque pratique : les fichiers .org sont plus agréables à lire avec emacs (couleurs, navigation, etc.)

Cours

Planning général

Supports de cours textuels

• Chapitre 0 (présentation) .org .html.
• Chapitre 1 (fonctions) .org, .html.
• Chapitre 2 (arbres) .org .html.
• Chapitre 3 (égalités) .org, .html.
• Chapitre 4 (arbres de preuve) .org,
  
• Chapitre 5 (relations inductives) .org,
  version .html.
• Chapitre 6 (langage While) .org,
  version .html.
• Chapitre 7 (égalités super-contagieuses, inversions) .org,
  version .html.
• Chapitre 8 (Sémantique Opérationnelle Structurelle de While) .org,
  version .html.

Supports de cours en Coq

• B A BA, version .html.
• B A BA en mode interactif, version .html.
• B A BA avec fonction "ouf", version .html.
• Récurrence sur propriété quantifiée, version .html (éventuellement partagé avec PF).
• Égalité booléenne sur nat, version .html.
• Sémantique naturelle du langage While : définition, version .html.
• Polymorphisme, arguments implicites, version .html.
• Sémantique naturelle du langage While : propriétés (début), version .html.
• Égalités super-contagieuses, inversions, version .html.
• SOS du langange While correspondant au chapitre 8., version .html

TD

• TD 01 ; aide : TD 01 dessin.
• Énoncé TD 02 : fichier coq à rendre en devoir à la maison.
  
• Énoncé TD 03 : fichier coq à rendre en devoir à la maison.
  Attention : il y a des questions facultatives à différents endroits, elles ne sont pas regroupées à la fin.
  NE PAS les traiter avant que le reste ait été fait, laissez les "Admitted" puis revenez-y dans un second temps en fonction de votre temps disponible.
  
• Énoncé TD 04 : fichier coq à rendre en devoir à la maison.
• Énoncé TD 05 partie 1 (relations inductives) : fichier coq à regarder pour le TD5.
• Énoncé TD 05 partie 2 (sémantique de While) : fichier coq à rendre en devoir à la maison.
• Énoncé TD 06+ (sémantique naturelle) : fichier coq.
  à rendre en devoir à la maison en plusieurs étapes.
• Énoncé TD 07 (sémantique opérationnelel structurelle) : fichier coq.
  avec notamment le matériel à réutiliser dans le projet final.
• Énoncé TD 08 (compilation certifiée) : fichier Coq.
  Compiler préalablement les définitions préliminaires : fichier Coq
  

Projet