Cours de L3 "programmation 1"
L'emploi du
temps.
- Cours: Mihaela Sighireanu (première partie), Jean Goubault-Larrecq (deuxième partie, documentée plus bas), les mardis de 13h30 à 15h30;
- TD: Julien Lamiroy, Stefan Schwoon, les lundis de 16h à 18h;
- Tutorat: les mardis de 9h à 10h;
- Projet: Margot Catinaud, Julien Lamiroy, Nicolas Margulies, les vendredis de 13h15 à 15h45;
Le contenu du cours
Le cours de programmation de 1ère année du l'année L3 se découpe en deux parties. Ceci est la page de la première partie. Elle-même se découpe en deux sous-parties.
De quoi sera-t-il question dans la première sous-partie?
- des différents styles de langages de programmation, avec un
accent particulier sur la programmation impérative (notamment en langage C), qui
est sans doute relativement nouvelle pour vous. On parlera aussi de
langages fonctionnels; il est probable que vous ayez déjà quelques
bases en OCaml,
mais on y parlera aussi d'autres langages, par exemple Lisp ou Rust.
- Il y sera aussi question des constructions typiques de chaque
famille de langages, des questions de portée (lexicale, opposée à la
liaison dynamique), de passage de paramètres, des constructions de
types de données, etc.
- A plus bas niveau, on verra comment tous ces objets sont
représentés en machine, et le cours s'interfacera notamment avec
celui d'architecture
et systèmes de Stefan
Schwoon.
- On s'exercera aussi à écrire de petits programmes, et des moins
petits, dans chacun de ces langages et chacun des styles permis ou
encouragés dans ces langages. Ceci se fera en séances de TP.
Tout ceci nous occupera, grosso modo, de septembre à novembre. Les
cours y seront assurés par Mihaela Sighireanu.
Et dans la seconde sous-partie?
De novembre à début janvier, nous profiterons des acquis pour
progresser vers:
- la sémantique des langages de programmation, autrement dit la
représentation mathématique de ce que les programmes font (ou
devraient faire). On parlera notamment de sémantique opérationnelle
à grands pas, et de sémantique dénotationnelle.
- L'intérêt principal d'une formalisation mathématique est d'établir
des théorèmes. On parlera donc de preuve sur des programmes, ou sur
des propriétés de langage de programmation.
- L'autre intérêt d'une sémantique est la documentation précise du
langage. Dans le cadre du projet,
on insistera donc sur le fait que le mini-compilateur de C que vous
aurez à réaliser respecte la sémantique proposée.
Les modalités d’examen sont grosso modo les suivantes. Elles
prennent en compte les composantes suivantes:
- D: partiel à mi-parcours (normalement en novembre), sous
forme de devoir à la maison;
- E: examen (janvier), portant essentiellement sur la
seconde partie du cours, mais pas nécessairement exclusivement;
- CC1, CC2: contrôle
continu, première resp. deuxième partie, moyenne des rendus en TD;
- P1: projet 1, allocateur mémoire, en C;
- P2: projet 2, compilation partie analyse, en OCaml.
La note finale sera:
0,4 E + 0,1 CC1 + 0,1
CC2 + 0,2 D + 0,1 P1
+ 0,1 P2
à condition que
P1 et P2 soient validés
(≥10/20). Si P1 ou P2
n’est pas validé, le module ne pourra pas être
validé.
Voici le sujet d’examen
2021/22, et son corrigé,
à titre d’exemple. De même, le sujet d’examen
2022/23, et son corrigé.
Le programme des cours
Ceci est un programme indicatif de la deuxième partie, sujet à évolution.
- Sémantique 1: les notes de cours.
Sémantiques opérationnelles d’un langage impératif jouet.
Voici la première série de transparents
de ce cours de sémantique, et la version
courte.
- Sémantique 2: les notes de cours. Sémantique
dénotationnelle, dcpos, théorèmes de points fixes. Voici la deuxième
série de transparents
de ce cours de sémantique, et la version
courte. La vidéo
du cours (2020).
- Sémantique 2, suite (mêmes notes de cours). Correction,
adéquation, équivalence contextuelle, logique de Hoare, weakest
preconditions. Voici la troisième série de transparents
de ce cours de sémantique, et la version
courte… mais nous terminerons d’abord la deuxième
série. La vidéo
de ce cours (2020).
- Sémantique 2, fin (mêmes notes de cours). Le langage fonctionnel
d’ordre supérieur PCF, sémantiques opérationnelle
dénotationnelle, clôtures, correction, adéquation. Voici la
quatrième série de transparents
de ce cours de sémantique, et la version
courte. La vidéo
de ce cours (2020): nous nous sommes arrêtés au transparent 7 de
cette dernière série de transparents.
- Sémantique 3: les notes de cours.
Typage, et plus spécifiquement de ML; l’algorithme
d’inférence de Hindley pour ML monomorphe, le problème de
l’unification. La vidéo
(2020); nous n’avions pas encore commencé à parler de typage,
qui est traitée dans la vidéo suivante. Les transparents,
et la version
courte.
- Sémantique 3, suite. La vidéo
(2020). Termes, substitutions, l’algorithme
d’unification, sa correction, unificateurs les plus généraux
(mgu).
- Sémantique 3, fin. Unification, fin: terminaison; théorème de
Milner (“well-typed programs do not go Wrong”),
algorithme W et typage de ML polymorphe. La vidéo
(2020).
- Optionnel: les bases de l'interprétation
abstraite, la théorie qui sous-tend l'analyse statique de
programmes, avec les transparents,
et la version
courte. La vidéo
(2020).
Last modified: Wed Oct 2 09:43:50 CEST 2024