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.
- Enseignant: Sylvain Salvati