Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Langages de programmation (48h, 6 ECTS)

Responsables : Giuseppe Castagna et Xavier Leroy

Plan du cours et intervenants prévus pour 2005-2006

  1. Langages fonctionnels et impératifs François Pottier 15
  2. Soustypage, langages à objets et XML Giuseppe Castagna 15
  3. Programmes logiques avec contraintes François Fages 6
  4. Langages concurrents avec contraintes Sylvain Soliman 12

Objectifs

Le but de ce cours est de présenter les concepts, principes et formalismes sous-jacents aux langages de programmation modernes. Il constitue une introduction à la recherche contemporaine sur les langages de programmation.

Ce cours aborde un large éventail de paradigmes de programmation: programmation fonctionnelle; programmation impérative; programmation par objets, avec une ouverture vers le traitement des données semi-structurées (XML); programmation par contraintes.

Le cours ne se contente pas de passer en revue des paradigmes de programmation. L'accent est mis sur les propriétés mathématiques des langages de programmation: sémantiques formelles (principalement sous forme de sémantiques opérationnelles), systèmes de types, et propriétés de fiabilité et de sécurité qu'assure le typage statique. Le cours présente les principaux systèmes de typage statique: monomorphe, polymorphe paramétrique, polymorphe par sous-typage, ainsi que les algorithmes de vérification et d'inférence de types associés.

Plan du cours

Langages fonctionnels et impératifs
Sémantiques à réduction pour les traits fonctionnels: liaison, fonctions, structures de données, récursivité.
Sémantiques à réduction pour les traits impératifs: structures de données modifiables; exceptions.
Systèmes de types: monomorphe; polymorphe paramétrique (système //F// et ML).
Sûreté du typage: propriétés d'auto-réduction et de progrès.
Inférence de types par production puis résolution de contraintes.
Traits avancés: types de données algébriques, types récursifs, annotations de types, typage structurel des enregistrements (rangées).
Langages à objets et XML
Rappels sur la programmation par objets.
Modèles typés d'objets: modèle à enregistrements et modèle à surcharge.
Méthodes binaires: le problème de la covariance.
Sous-typage; correction et complétude des algorithmes de sous-typage; sous-typage du second ordre (//F//<:); polymorphisme F-borné; sous-typage des types récursifs.
Sous-typage sémantique: types réguliers d'arbres et leur application au typage des documents XML.
Langages de transformation pour XML (CDuce).
Langages à contraintes
Programmes logiques avec contraintes sur le domaine de Herbrand, les domaines finis, les booléens et les nombres réels.
Algorithmes de résolution de contraintes par réduction. Algorithmes de propagation de contraintes.
Sémantiques opérationnelles, de point fixe et logiques.
//Model checking// avec contraintes.
Langages concurrents avec contraintes; sémantiques opérationnelles et dénotationnelles.
Sémantique en logique linéaire; systèmes de contraintes pour les traits impératifs.

Pré-requis

Il est recommandé d'avoir suivi les cours de première année Compilation et Sémantique des langages de programmation. <br />Notions élémentaires de sémantique opérationnelle (avoir déjà vu des règles de réécriture et des règles d'inférence). <br />Expérience de et goût pour la programmation. <br />Notions de Caml et/ou de Java.

Bibliographie

  • //Types and Programming Languages//, Benjamin C. Pierce, MIT Press, 2002.
  • //Principles of Constraint Programming//, Krzysztof Apt, Cambridge University Press, 2003.

Intervenants

G. Castagna CR CNRS LIENS
F. Pottier CR INRIA Rocquencourt
F. Fages DR INRIA Rocquencourt
S. Soliman CR INRIA Rocquencourt

Planning

  • FI = Langages fonctionnels et impératifs
  • OX = Langages à objets et XML
  • CO = Langages à contraintes
Date Cours Contenu
04/10 FI cours 1
11/10 cours 2
12/10 cours 3 (ATTENTION exceptionellement un mercredi!)
18/10 cours 4
25/10 cours 5
01/11 férié
08/11 OX cours 1
15/11 cours 2
22/11 cours 3
29/11 cours 4
06/12 cours 5
13/12 FI+OX examens
20/12 vacances de Noël
27/12
03/01 CO cours 1 - Introduction, logique, contraintes
10/01 cours 2 - CLP, points fixes
17/01 cours 3 - CLP, sémantique logique
24/01 pas de cours
31/01 CO cours 4 - CC, sémantique opérationelle, exemples
07/02 cours 5 - CC, sémantique logique linéaire
14/02 cours 6 - LCC, !SiLCC - Attention! Salle W
21/02 examen - Attention! Salle W
 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA