Master informatique

SEM : Description sémantique des langages de programmation

  • Mention du master : informatique
  • Parcours : « génie logiciel »
  • Semestre : (de 1 à 4) : 1

Objectifs

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.Savoir et savoir-faire associés

Savoir et savoir-faire associés

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.

Prérequis

Notions de programmation fonctionnelle et de logique

 

Informations pratiques

  • Responsable U E : David Cachera
  • Composante : ENS
  • Crédits U E : 5
  • Capacité d'accueil : 20 étudiants
  • Langue d'enseignement : français
  • Forme de l'enseignement : (présentiel, visio, à distance,....) : présentiel
  Cours T.P. T.D Projet Stage
Présentiel par étudiant 24h   24h    
Travail personnel par étudiant 12h   24h 24h