Sémantique (SEM)

Description

Cette UE fait partie du M1 informatique mais peut être suivie en M2, dans le cas où l'étudiant-e ne l'aurait pas suivi en M1. 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.

Mots-clés

Sémantique des langages de programmation, Preuve formelle

Prérequis

Des bases de programmation fonctionelle et de logique rudimentaire (quantificateurs, implication)

Contenu

Programmation fonctionnelle en Coq
Types inductifs et preuves par induction
Tactiques de preuve et logique en Coq
Syntaxe et sémantique d’un langage impératif
Compilation vers une machine à pile
Sémantique opérationnelle à petits pas
Typage
Aspects plus avancés des langages impératifs et fonctionnels

Compétences acquises

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.

Enseignants

David Cachera (responsable), Sandrine Blazy