IFT 6172 -- Sémantique des langages de programmation


Professeur: Stefan Monnier
Premier cours: vendredi 9 Janvier 2014, 13h30-15h30, salle AA-1409


Page Moodle du cours pour H2014.

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, Coq ou Agda.

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
Mardi 13h30-15h30 AA-1177
Vendredi 13h30-15h30 AA-1409

Voir aussi le formulaire insupportable de Synchro

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

Manuels

Il n'y a pas de manuel pour ce cours, cependant les livres ci-dessous pourraient être de bons compléments au cours:

Types and Programming Languages de Benjamin C. Pierce, MIT Press.

Computation and deduction de Frank Pfenning (aussi en 2-up).

Lambda Calculi with Types de Henk Barendregt (aussi en 2-up).

Certified Programming with Dependent Types de Adam Chlipala.

Semantics of Programming Languages, Structures and Techniques, Carl A. Gunter, MIT Press.

Planification par semaine

Semaine du Thème
9 jan
13-16 jan
20-23 jan
27-30 jan
3- 6 fév
10-13 fév
17-20 fév
24-27 fév
3- 6 mar Relâche
10-13 mar
17-20 mar
24-27 mar
0- 3 avr
7-10 avr
14 avr

Présentations


Articles suggérés

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.

Linear Regions Are All You Need, Matthew Fluet , Greg Morrisett , Amal Ahmed, ESOP'06.

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

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

Staged computation

Environment classifiers, Walid Taha and Michael Florentin Nielsen, POPL'03.

Co-inductive types

Copatterns: the final approach to codata?, Andreas Abel and Brigitte Pientka, ICFP'13.

Linear types

Propositions as Sessions Philip Wadler, ICFP 2012.

Linear Regions Are All You Need, Matthew Fluet , Greg Morrisett , Amal Ahmed, ESOP'06.

Linear types can change the world!, Philip Wadler, 1990.

Modal types

Contextual modal type theory, Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka, 2008.

Session types

Haskell Session Types with (Almost) No Class, Riccardo Pucella and Jesse A. Tov, Haskell'08.

Propositions as Sessions Philip Wadler, ICFP 2012.

Parametricity

Theorems for free! Philip Wadler, ICFP'89.

Parametricity as subtyping, QingMing Ma, POPL'92.

The Girard-Reynolds isomorphism (second edition), Philip Wadler. TCS, 2007.


Software

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