Archive 2019
Validationprojet
EnseignantPierre Letouzey
Horaires hebdomadaires 2 h CM , 2 h TP
Années Master Logique et Fondements de l'Informatique

Syllabus

Attention, ce cours aura lieu les 6 dernières semaines du 1er semestre et les 6 premières semaines du 2nd semestre.

Une moitié des heures de ces modules consistera en des cours, l’autre en des TP sur machine. Ces cours se concluront par un projet à réaliser en Coq. Le contenu de ces cours est un prérequis pour le cours de théorie des types homotopiques.

Sommaire

Programmation fonctionnelle en Coq

  • Lambda-calcul, récursivité (et ses limites en Coq), typage à la ML
  • Structures de données usuelles (booléens, entiers, listes, options, arbres, ...)
  • Programmation générique : polymorphisme, modules, classes de type
  • Types dépendants
  • Lien avec d'autres langages comme OCaml, présentation des "absents" de Coq (exceptions, traits impératifs, entrées-sorties, ...), comment faire le lien entre OCaml et Coq

Preuves formelles en Coq

  • Langage de spécification, règles logiques de base
  • Arithmétique, calcul, réécriture, récurrence
  • Preuves de propriétés des structures de données usuelles
  • Prédicats inductifs
  • Automatisation
  • Éventuellement: rapide tour d'horizon d'autres assistants de preuves et comparaison avec Coq

Bibliographie