Calculabilité et complexité

Nous utiliserons essentiellement les documents rédigés par Yannick Le Bras que je mets à jour régulièrement. Voici le planning de l'UE :
  1. Culture informatique, indécidabilité du problème de l'arrêt ; intro à Coq
  2. Terminaison 1 ; exos
  3. Terminaison 2 ; exos
  4. Terminaison 3 ; exos
  5. Correction 1 ; exos terminaison 30 et 33
  6. Révisions ; exo 34; vidéo : Vérification déductive des programmes
    -- partiel
  7. Correction 2 ; exos
  8. Correction 3 ; exos
  9. Notations asymptotiques, complexité 1 ; exos
  10. Complexité 2 ; exos
  11. Complexité 3 ; exos 1.3 et 2.1 de la fiche d'exos Complexité algorithmique
  12. Complexité 4 ; exos : complexité des algos 16-18 de la fiche de cours Terminaison, 2.2 et 4 de la fiche d'exos Complexité algorithmique
    -- partiel

Cours

  1. Eléments de culture scientifique informatique, indécidabilité du problème de l'arrêt
  2. Terminaison
  3. Correction
  4. Notation asymptotique : O() et Θ() (Sylvie Hamel)
  5. Complexité algorithmique

Exercices

  1. Exercices introductifs
  2. Exercices sur les notations asymptotiques
  3. Complexité algorithmique (Etienne Payet)

Travaux pratiques

Une initiation au système Coq (téléchargement) à partir des premiers chapitres de l'ouvrage collectif Software Foundations traduits en français par Tom Hirschowitz.
  1. Exercices introductifs
  2. Les bases, squelette
  3. L'induction, squelette
  4. Quiz Coq #1 (David Pichardie)
  5. Les structures de données, squelette

Evaluation

Contrôle continu : deux partiels sans document ni moyen électronique, 50% + 50%.
Deuxième session : examen écrit sans document ni moyen électronique, tout est au programme, 100%.

Annales


Valid HTML5