Sémantique des langages de programmation

Programmation fonctionnelle. Connaissances de base en logique.

La justification rigoureuse d'un travail scientifique constitue une part importante de l'activité de recherche en informatique. Ce cours a pour objectif de donner les éléments pour être capable de démontrer rigoureusement des propriétés portant sur les langages de programmation et les programmes écrits dans ces langages.

Une sémantique formelle permet de décrire de façon non ambiguë le comportement attendu d'un programme. Il est par exemple possible d'établir la correction d'un compilateur en prouvant que le programme source et le programme compilé montrent les mêmes comportement observables par rapport à une sémantique donnée. Le cours étudiera différentes formes de sémantiques pour différentes caractéristiques de langages de programmation.

L'implémentation des sémantiques et la vérification de leurs propriétés se fera via l'assistant de preuve Coq. Cet outil est utilisé pour vérifier la correction de chaque étape élémentaire d'une preuve. Les cours seront donnés avec cet outil, et les étudiants l'utiliseront à la fois pendant les séances de cours et de TD. Les échanges entre enseignants et étudiants, et entre étudiants, se feront via un forum (piazza). À la fin du cours, l'étudiant sera capable de spécifier et de prouver des  propriétés non triviales d'un langage de programmation.

Examen terminal et contrôle continu