ilu3-coq-alectryon

Au sein de la Mention Informatique de la Licence Flexible de l'Université Toulouse III - Paul Sabatier, l'UE Ingénierie des Logiciels et Utilisabilité 3 (prévue essentiellement au niveau L3) se focalise sur le Développement Dirigé par les Types Abstraits.

Cette page regroupe les supports de cours pour la partie Coq.

Supports de Cours/TD

Il y a une page HTML par cours, générée (avec les outils Alectryon et docker-coq-action) à partir des sources Coq :

• Cours 1 : ilu3_coq_1.html - ilu3_coq_1.v (fragment fonctionnel de Coq)
• Cours 2 : ilu3_coq_2.html - ilu3_coq_2.v (tactiques de preuve)
• Cours 3 : ilu3_coq_3.html - ilu3_coq_3.v (modules & types abstraits)

Environnement de TP

Si vous disposez d'une machine personnelle, vous pouvez installer l'environnement de TP (OPAM+Coq+ProofGeneral) en suivant ce tutoriel :

• https://github.com/erikmd/tapfa-init.el

✨ 🐓 ✨