IFT 6172 -- Sémantique des langages de programmation


Professeur: Stefan Monnier
Plan du cours
Premier cours: mercredi 7 Janvier, 14h30-16h30, salle Z-205


Description

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.

Horaire et dates

Jour Heure Lieu Type
Mercredi 15h00-17h00 Z-205 Cours
Vendredi 13h30-15h30 AA-1411 Cours

Voir aussi la page du programme des cours.

Évaluation

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.

Travaux pratiques

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.

Manuels

Il n'y a pas de manuel pour ce cours, cependant les livres cités ci-dessous seront de bonnes aides pour suivre le cours, ou de bons compléments sinon.

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)

Présentations

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?

Articles potentiels

Memory management

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.

Information flow

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.

Type inference

Principal type-schemes for functional programs, Luis Damas and Robin Milner, POPL'82.

MLF

Compilation techniques

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.

Trustworthy programs

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.

Dependent types

Fun with phantom types, Ralf Hinze.

Eliminating Array Bound Checking Through Dependent Types, Hongwei Xi and Frank Pfenning, PLDI'98.

GADTs

Types

A Syntactic Approach to Type Soundness, Wright and Felleisen (in Information and Computation).

Unclassified

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


Software

Voir la page séparée pour les systèmes Twelf et Coq.
Stefan Monnier
Best viewed with ANY browser