Ce cours est assuré par Pierre Lescanne assisté
de Daniel Hirschkoff.
L'objet de la sémantique est fondamentalement d'associer du sens à des composants d'un langage. Pour nous ce seront les différents éléments d'un programme.
Le sens est un objet mathématique à définir, sur lequel on peut faire des manipulations formelles et des preuves.
Dans ce cours, on souhaite montrer qu'il est possible de donner une description mathématique rigoureuse de concepts introduits souvent informellement dans les cours de programmation: les programmes sont des objets mathématiques comme les autres. Les outils mathématiques nécessaires à cette description seront présentés au début du cours dans un cas restreint et complétés au fur et à mesure des besoins.
Dans la première partie de ce cours, nous étudierons les concepts de la sémantique sur un langage impératif de type Pascal à savoir
Ensuite nous aborderons les concepts fondamentaux de la sémantique sur le lambda-calcul où les problèmes apparaissent sur leur jour mathématique le plus pur. Ensuite, nous étudierons les calculs pour la mobilité et la communication, notamment le pi-calcul.
Voici les transparents du cours. Je maintiens ces liens à jour, pour prendre en compte les coquilles que je remarque. Mais en général, la version la plus à jour est sur l'espace pédagogique de l'ENS de Lyon.Les sources LaTeX sont fournis (voir les répertoire OUTILS pour y trouver les fichiers spécifiques que j'utilise)
Pour les travaux dirigés, je vous invite à aller consulter la page de Daniel Hirschkoff.
Voici un article de Carl Gunter sur les programmes micro-mobiles Pour trouver l'article de John Reynolds sur la preuve de programmes avec des références visitez Separation Logic: A Logic for Shared Mutable Data Structures sur sa page