Il est important d'installer Isabelle et de vérifier que cela fonctionne en ouvrant ce tutoriel avant la première séance. Le tutoriel sera fait lors de la première séance de cours.
Séance 1/5 le 2 février 2026
- Introduction
- Prise en main d'Isabelle/HOL avec le tutoriel et quelques exercices
Séance 2/5 le 6 mars 2026
- Rappels sur la sémantique
- Syntaxe abstraite de Niklaus : expressions, instructions
- Sémantique naïve par interprétation
- Sémantique opérationnelle de Niklaus
- Exemples (curryfication et définition de fonctions inductives)
Exercices à rendre sur le dépôt git (avant la dernière séance) :
Séance 3/5 le 13 mars 2026
- Sémantique dénotationnelle
- Sémantique des définitions récursives
- Points fixes, théorème de Knaster-Tarski
Séance 4/5 du 20 mars 2026
- Sémantique axiomatique, triplets de Hoare.
- Plus faible précondition, Consistance et complétude
- Exemple de preuve de programme Niklaus
Pour un exemple assez simple de preuve de correction d'un compilateur,
vous pouvez consulter l'épisode Program correctness
de la chaîne Youtube Computerphile.
J'ai fait la preuve de la correction du mini compilateur sur cette page.
Séance 5/5 du 27 mars 2026
- Compléments
- Aide pour finir les exercices à rendre
Récapitulatif des exercices à rendre avant le 20 avril 2026
- Fichiers complétés en cours (sémantiques, récursion etc.)
- Exercices :
- Tutoriel et exercices associés
- Simplification d'expressions Niklaus
- Compilation d'expressions Niklaus
- Modélisation d'expressions régulières
Séances Frama-C les 30 mars et 3 avril 2026
Attention, projet à rendre aussi sur ce sujet.