INFO3104 : Théorie de la programmation

Ce cours présente un ensemble de méthodes permettant de définir mathématiquement ce qu'est un programme, et comment il s'exécute. Une telle approche permet de formuler et prouver des propriétés portant sur le comportement des programmes (absence de bugs, conformité vis-à-vis d'une spécification attendue).
Voici une liste indicative des notions couvertes en cours :

• définitions inductives d'ensemble et de relations ; preuves par induction
• sémantique opérationnelle, sémantique détnotationnelle
• éléments de réécriture : terminaison, confluence, paires critiques, unification du premier ordre
• typage pour un petit langage fonctionnel
• logique de Floyd-Hoare, logique séparante
• preuve formelle à l'aide de l'assistant de preuves Coq