Ce cours présente les techniques formelles utilisées pour décrire et analyser la sémantique statique et dynamique des langages de programmation.
Le but du cours est de se familiariser avec les techniques de spécification formelles des langages de programmation, ainsi que les outils utilisés pour spécifier, analyser, et prouver diverses propriétés intéressantes, telle que la préservation des types.
Le cours utilisera des exemples concrets codés dans des langages tels que Twelf et Coq.
Les sujets couverts suivront les lignes suivantes:
Ces sujets seront vu avec en arrière plan, comme application principale, les techniques de sécurité basée sur le langage, telles que popularisées par Java. Plus spécifiquement, le cours inclura aussi une partie où l'on verra comment ces techniques développées pour décrire et analyser formellement la sémantique des langages peuvent s'appliquer à la spécification et la vérification formelle de programmes.
Les méthodes formelles sont déjà très utilisées dans le design de systèmes logiques, mais beaucoup moins dans le domaine du logiciel. Toutefois cela est en passe de changer à cause des problèmes de sécurité récurrents. Les techniques présentées dans ce cours, originalement développées dans le cadre de la logique mathématique et de la théorie des langages, sont parmi les plus prometteuses pour augmenter la fiabilité des programmes de demain.
La deuxième moitié du cours sera structurée autour de présentations d'articles de journaux et de conférences.
| Jour | Heure | Lieu | Type |
|---|---|---|---|
| Mercredi | 15h00-17h00 | Z-205 | Cours |
| Vendredi | 13h30-15h30 | AA-1411 | Cours |
Voir aussi la page du programme des cours.
Chaque étudiant devra faire 2 travaux pratiques et 2 présentations. La note sera basée pour 50% sur les travaux pratiques, 40% sur les présentations et 10% sur la participation en classe.
Le TP1 est à rendre par email avant le 18 mars à midi. Le source LaTeX de la donnée est aussi disponible, pour ceux qui veulent s'en inspirer.
Le TP2 est à rendre par email avant le 22 avril à minuit. Le source LaTeX de la donnée est aussi disponible, pour ceux qui veulent s'en inspirer.
Types and Programming Languages de Benjamin C. Pierce, MIT Press.
Semantics of Programming Languages, Structures and Techniques, Carl A. Gunter, MIT Press.
Computation and deduction de Frank Pfenning (aussi en 2-up).
Lambda Calculi with Types de Henk Barendregt (aussi en 2-up)
| Jours | Sujet |
|---|---|
| 3 Avr | Michael: Separation Logic: A Logic for Shared Mutable Data Structures |
| 8 Avr | Darin: "A Universe of Partial Computations for Coinductive Type-Theoretic Semantics" (lectures préalables: AgdaIntro, et A Coinductive Monad for Prop-Bounded Recursion) |
| 10 Avr | Férié: vendredi saint |
| 15 Avr | Christian: Mixin' Up the ML Module System |
| 17 Avr | Michael: Foundational Proof-Carrying Code |
| 22 Avr | Darin: Observational Equality, Now! |
| 24 Avr | Christian: Composable and Compilable Macros: You Want it When? |
Typed Memory Management in a Calculus of Capabilities, Karl Crary, David Walker, and Greg Morrisett, POPL'99.
Alias types, Frederick Smith, David Walker, and Greg Morrisett, ESOP'00.
Separation Logic: A Logic for Shared Mutable Data Structures, John Reynolds, LICS'02.
Secure Information Flow and CPS, Steve Zdancewic and Andrew C. Myers, ESOP'01.
Translating dependency into parametricity, Stephen Tse and Steve Zdancewic, ICFP'04.
A Modal Foundation for Secure Information Flow, Kenji Miyamoto and Atsushi Igarashi, FCS'04.
Principal type-schemes for functional programs, Luis Damas and Robin Milner, POPL'82.
MLF
Representing Control: A Study of the CPS Transformation, Olivier Danvy and Andrzej Filinski, Mathematical Structures in Computer Science 2(4), 1992.
The essence of Compiling with Continuations, Cormac Flanagan, Amr Sabry, Bruce F. Duba, Matthias Felleisen, PLDI'93.
Precision in Practice: A Type-Preserving Java Compiler, Christopher League, Zhong Shao, and Valery Trifonov, CC'03.
Proof-Carrying Code, George C. Necula, POPL'97.
From System-F to Typed Assembly Language, Greg Morrisett, David Walker, Karl Crary, and Neal Glew, POPL'98.
Foundational Proof-Carrying Code, Andrew Appel, LICS'01.
A Type System for Certified Binaries, Zhong Shao, Bratin Saha, Valery Trifonov, and Nikolaos Papaspyrou, POPL'02.
Fun with phantom types, Ralf Hinze.
Eliminating Array Bound Checking Through Dependent Types, Hongwei Xi and Frank Pfenning, PLDI'98.
GADTs
A Syntactic Approach to Type Soundness, Wright and Felleisen (in Information and Computation).
Parametricity as Subtyping, QingMing Ma, POPL'92.
Environment Classifiers, Walid Taha and Michael Florentin Nielsen, POPL'03.
Low-level code: - parametricity for continuations - existentials for closures - the need for ABC-elimination - the need to separate alloc from init - the need to separate switch from field-access - object encodings
| Stefan Monnier |
|