Sémantique des Langages de Programmation
Master 1 Informatique 2022–2023
Table des matières
1. Introduction
Bienvenue sur la page du cours de sémantique des langages de programmation.
L'enseignement a lieu chaque semaine le lundi en salle 2001 du bâtiment Sophie Germain, le cours magistral de 14h à 16h, les travaux dirigés de 16h15 à 18h15.
2. Support de cours
Les notes de cours sont disponibles. Chaque chapitre se termine par une liste d'exercices pratiqués en travaux dirigés.
Le document est en évolution permanente, merci de me signaler toute erreur ou imprécision.
3. Journal du cours
3.1.
3.1.1. Introduction
- Quoi ?
- Une introduction à la théorie des langages de programmation.
- Un cours d'informatique mathématique.
- L'informatique mathématique est à l'informatique ce que la physique mathématique est à la physique : une étude idéalisée et très précise des objets de la discipline, épurés de leurs caractéristiques contingentes.
- Un cours probablement difficile si on est complètement réfractaire aux
mathématiques et à la logique.
- Pas de prérequis mathématiques sauf savoir manipuler des ensembles et faire des preuves par induction. Ce qu'on va réviser.
- Pas de mathématiques vraiment difficiles, mais je vous demanderai de faire des preuves en TD et à l'examen.
- La continuation naturelle d'un cours de logique de licence, et aussi en
quelque-sorte la suite d'un cours de compilation.
- On va donner un sens aux langages de programmation informatique en les traduisant en objets mathématiques. C'est une forme de compilation abstraite bien particulière.
- Pourquoi ?
- Préparer à la recherche en langages de programmation, publique ou privée.
- Donc, préparer les étudiants qui envisagent de faire une thèse.
- Naturellement MPRI, mais aussi des autres parcours, notamment LP.
- Vous entraîner aux raisonnements mathématiques qu'on attendra de vous dans un master 2 orienté recherche.
- Comment ?
- Format classique : 2h de CM et 2h de TD par semaine.
- Évaluation : contrôle continu + devoir + examen terminal.
- Des notes de cours à lire impérativement pour assimiler le contenu du cours.
- Remarque : synergie avec le cours de preuve assistée par ordinateurs du vendredi.
3.1.2. Contenu des notes traité ce jour
Chapitre 2 jusqu'à la définition de la substitution naïve et la preuve du corollaire 1.