Cette page est la page officielle de la partie " Typage " du cours du 1er semestre 2022/2023 intitulé
« Typage et Analyse Statique »
qui s'adresse aux étudiants de master de Sorbonne-Université.
Nouvelles fraîches
- 1er cours : jeudi 21/09/2023 à 8h30 (salle 55-66 105) et à 10h45 en salles 14-15 507 et 509.
Notes de cours, TD et TME
- 6ème cours
- polymorphisme parametrique en Java, lambda-expressions en Javai, fusion des modèles (PDF)
- finalisation des attributions d'articles
- avancement du typeur
- compléments :
- présentation du typage graduel, tutorial Jeremy Siek à POPL 2017 (lien)
- un mot sur le système de types de Rust, présentation de Testard à l'OSIS 2016, scope sur doc.rust-lang.org
- 5ème cours : surcharge en Java et Haskell (PDF)
- comparaison algorithmes de résolution de la surcharge en Java 1.5
et en java 1.2
- simulation d'algorithme de surcharge en Java 1.5 avec production de code ZAM (projet Potdevin-Vaugon) (rapport et javaz.tgz)
- simulation d'algorithme de surcharge de Dul et Maslia (rapport et jar)
- surcharge en Haskell, testez les exemples du cours en ghc (ghc) : try Haskell
- tester les fonctions récursives en CLOS
- détermination des projets de chaque groupe (voir site moodle du cours)
- 4ème cours : polymorphisme par sous-typage structurel (en OCaml) et nominal (en Java) : PDF (chapitre 15 de DA-OC).
- réalisation du devoir sur le typeur
- exercices sur les méthodes binaires en ocaml avec héritage n'est pas sous-typage
- présentation des articles, lien sur moodle (à venir)
- 3eme cours : typage d'un mini-ML (PDF)
-
test d'un typeur (cf lien) d'un mini-ML
- version sans analyse syntaxique en OCaml (lien) o
u Fsharp (lien).
- suivre le fichier d'exemples (cf lien).
- ajout des traits impératifs à un typeur (cf lien), avec le fichier de tests (lien).
- ajout d'une coercition de type : (e : type)
- si vous ne connaissez pas OCAML,
- suivez le cours OUV (ouverture) des M1 STL
- projet de programmation : présentation en TME, sujet sur moodle
- code d'un typeur en ML à base de contraintes
- 2ème cours : lambda-calcul simplement typé (PDF)
-
Programmes et documents :
- construire les arbres de typage des termes suivants :
- K I I
- idendité : I I = (\x.x)(\x.x)
- S K K (correction)
- montrer que \ab.(a b)(b a) n'est pas typable.
- sur les entiers de Church : add 2 2
- que déduire des types de I et 2 ?
- lire et tester un typeur en OCAML, utilisable avec tryocaml, ou typeur en F#.
- typeur d'un lambda-calcul, source, avec entier et add, résolution d'équations
- si besoin de mise à niveau en ocaml :
cours intro OCaml : Cours d'ouverture (M1)
- TD2 (exos 1.1, 1.2, 1.3, lire 2 et 3)
- 1er cours : présentation du semestre (PDF) et lambda-calcul pur (transparents : PDF)
- TD1
-
Programmes et document :
Équipe pédagogique
L'équipe pédagogique est ainsi constituée:
Emmanuel Chailloux (LIP6), Romain Demangeon (LIP6), Antoine Miné (LIP6), Milla Valnet (LIP6).
Pour envoyer un courrier à l'équipe pédagogique, cliquez ici.
Examens et notation
L'évaluation de ce module comprend :
- partie typage pour 50%
- présentation d'article
- projet initié en TME
- sur la partie analyse statique pour 50%
- présentation d'article
- projet initié en TME
Langages et environnements de travail
Bibliographie
Quelques lectures autour de la fiabilité logicielle et des langages :
Ouvrages de référence :
- sur le typage
- Types and Programming Languages - B. Pierce - The MIT Press
- sur l'analyse statique
- Principles of Program Analysis - F. Nielson, H. Nielson et C. Hankin - Springer
Autres liens
Remarques?
dernière modification : 25/10/2023