Sémantique des Langages de Programmation
Master 1 Informatique 2023–2024
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.
Nouveau : le sujet du devoir maison est disponible, tout comme l'archive des fichiers à compléter. Le devoir est à rendre jusqu'au 20 mai à 19h00 au plus tard.
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. Cours 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'à §2.3.1.
3.2. Cours 2
3.2.1. Contenu des notes traité ce jour
Chapitre 2 jusqu'à §2.4.2 inclus.
3.3. Cours 3
3.3.1. Contenu des notes traité ce jour
Fin du chapitre 2 et chapitre 3.
3.4. Cours 4
3.4.1. Contenu des notes traité ce jour
Chapitre 4 jusqu'à 4.1.3.
3.4.2. À faire pour la prochaine fois
Démontrer l'énoncé suivant.
Propriété : soit \(M\) un magma pointé et \(E\) une relation d'équivalence sur \(M\). La clôture compatible de \(E\) est transitive.
3.5. Cours 5
3.5.1. Contenu des notes traité ce jour
Chapitre 5 jusqu'au lemme de Newman exclu.
3.6. Cours 6
3.6.1. Contenu des notes traité ce jour
Chapitre 5 dans son intégralité.
Retour sur le chapitre 4.
3.6.2. À faire pour la prochaine fois
Exercices 25 et 26.
Réfléchir à la normalisation forte et à la confluence locale du système de réécriture qui implémente la théorie équationnelle des monoïdes.
3.7. Cours 7
3.7.1. Contenu des notes traité ce jour
Chapitre 4 jusqu'a la définition 38.
3.7.2. Code source
Le code écrit durant la séance est disponible.
3.8. Cours 8
3.8.1. Contenu des notes traité ce jour
Chapitre 6 jusqu'à §6.2.2.
3.9. Cours 9
3.10. Cours 10
3.10.1. Contenu des notes traité ce jour
Chapitre 6 jusqu'au modèle ensembliste inclus.
Note : le modèle ensembliste du système T a été présenté en cours via des notations légèrement différentes de celles utilisées dans les notes. Les notations utilisées en cours sont à privilégier.
3.11. Cours 11
3.11.1. Contenu des notes traité ce jour
Chapitre 6 jusqu'à la fin.
Le chapitre sur PCF des notes n'a pas été traité et n'est pas rédigé dans un style cohérent avec ce qui précède.