Cette page est la page officielle du cours du 1er semestre 2016/2017 intitulé
« Typage et Analyse Statique »
qui s'adresse aux étudiants de master de l'UPMC.
La description de la brochure du module se trouve
ici.
Nouvelles fraîches
- planning des soutenances cliquer ici
- consignes dans la rubrique Examens pour le choix et la remise du devoir sur le typage (article ou réalisation)
- colloqium LIP6 (du 11/10/16 à 17h45) : de Richard Stallman sur les logiciels libres (lien)
- colloqium LIP6 (du 29/09/16 à 18h) : de Patrick Cousot sur l'interprétation abstraite (lien)
- MOOC OCAML : début des courts le 26/09/16 : suivre le lien
- 1er cours : jeudi 22/09/2016 à 8h30 (salle 54-55 205) et à 10h45 en salles STL et salle 407 (14-15)
Notes de cours, TD et TME
- 6ème : GADT, fusion des modèles
- GADT en OCaml et panorama des langages (PDF et lien du manuel)
- présentation de Scala (Page Martin Odersky), dont une présentation popl06, tutoriel et présentation par l'exemple
- exercices :
- faire tourner le programme suivant en java 1.8 TestLambda.java
- traduire les fonctions fold_left, fold_right, map2, ..., du module List d'OCaml en java 1.8
- faire passer le typeur de lambda-termes et le typeur du mini-caml sous Scala (ou F# ou Swift), et ajouter un affichage.
- programmes OCaml avec GADT (lien du manuel) à faire tourner.
- vidéo sur Hack, cliquez sur le lien
- un exemple en Swift (main.swift), exemples du cours
- 5ème cours : polymorphisme parametrique et lambda-expressions en Java (PDF)
- passage du modèle Visiteur en generics (partiel nov2012 (LI314))
- utilisation de l'API stream (exemples des transparents)
- implantation des exemples avancés du tutorial de Pizza (lien)
- fin du choix des projets
- 4ème cours : typage objet et surcharge (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) : compilation en ligne, ou try Haskell
- détermination des projets de chaque groupe (voir rubrique Examens)
- 3ème cours : sous-typage structural en programmation objet, typage objet en Ocaml (PDF) - cours 7 et 8 de mpil 2015/2016 et chapitre 15 de DA-OC).
Exercices :
- Lire, tester et ajouter des traits impératifs à un typeur (cf lien), avec détection des expressions expansives.
- Adapter le texte du partiel de novembre 2012 de LI314 (cf lien) sur un visiteur paramétré en OCaml
(questions 1 à 4).
- Adapter en Java l'exemple des points avec méthodes binaires du cours.
- 2ème cours : lambda-calcul simplement typé
et typage d'un mini-ML fonctionnel et impératif (PDF)
-
typeur en OCAML ou typeur en F# (nouvelle version du 02.10.12).
- utilisation possible de tryocaml
- cours MPIL de L3,
- environnements : OCaml (Tuareg, Ocaide), F# (Visual studio sous Windows ou mono)
)
- MOOC OCaml (ouverture septembre 2016, inscription maintenant, cela vient juste de commencer)
-
test d'un typeur (cf lien) d'un mini-ML ou implantation du typeur en Scala, Swift ou Haskell
- suivre le fichier d'exemples (cf lien).
- ajout des traits impératifs à un typeur (cf lien).
- environnements en ligne :
- try ocaml : suivre le lien
- try F# : suivre le lien
- try Scala : suivre le lien
- try Haskell : suivre le lien
- 1er cours : présentation du semestre (PDF) et lambda-calcul pur (transparents : PDF)
- Exercices
- effectuer à la main (ou avec un logiciel en ligne) les réductions suivantes :
- Forme normale
Soient les termes suivants :
A =\xy.xy
DELTA = (\x.xx)
K = \xy.x
S = \xyz.xz(yz)
B = \xyz.(x(yz))
C = \xyz.(xzy)
Donner si elle existe la forme normale des termes suivants :
I = SKK,
B = S(KS)K,
OMEGA = DELTA DELTA,
C = S (BBS)(KK),
- Trouver les lambda-termes qui calculent la multiplication et la puissance pour les entiers de Church.
- implanter un évaluateur de lambda-calcul et le tester
- tester la représentation des listes (comme données sur le lien lien wikipedia)
- divertissement : lire la page sur "Alligator Eggs", voir le lien avec le lambda-calcul
-
Programmes et document :
Équipe pédagogique
L'équipe pédagogique est ainsi constituée:
Emmanuel Chailloux (LIP6), Romain Demangeon (LIP6), Antoine Miné (LIP6), Sarah Zennou (Airbus).
Pour envoyer un courrier à l'équipe pédagogique, cliquez ici.
Examens et notation
L'évaluation de ce module comprend :
- partie typage
- examen écrit (sur la partie typage) = 30% de la note
quelques sujets : 2011, 2012,
2013
- une étude sur un article ou une mini-réalisation sur le typage comptant 20% de la note
à choisir dans
cette
liste (version du 20/10/2016)
voeux :
indiquer en CLIQUANT ICI et en précisant au moins 3 voeux d'articles ou réalisations. Vu les délais courts, on essaiera de valider le choix dans les 48h (hors week-end)
remise rapport (et réalisation) :
à remettre en CLIQUANT ICI pour soumettre votre rapport (et réalisation avant le lundi 31/10/16 23h59)
remise transparents (en PDF) : à remettre en CLIQUANT ICI pour soumettre les transparents de votre exposé avant le mercredi (02/11/16) 17h.
-->
- sur la partie analyse statique
- interrogation(s) (10% de la note)
- présentation d'article (20% de la note)
- projet initié en TME (20% de la note)
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 : 08/11/2016