Cette UE est une introduction au raisonnement sur les programme. Elle
  s'appuie sur le logiciel Coq qui fournit un langage de programmation
  fonctionnelle ainsi que des moyens de raisonner sur les programmes.
  Elle abordera :
  - les rudiments de la programmation fonctionnelle en Coq,
  - la spécification des propriétés des programmes,
  - leur démonstration en coq.
  Coq est un assistant de démonstration, il prend en charge les aspects
  techniques des démonstrations pour ne laisser à l'utilisateur qu'à
  expliciter les raisons pour lesquelles un programme est correct. La
  dimension interactive de Coq rend les activités de programmation et de
  démonstration largement complémentaires et plaisantes.