WikiMPRI

This is an old, obsolete page: please go to Functional programming and type systems (48h, 6 ECTS) instead.

Responsables : Giuseppe Castagna et Xavier Leroy

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

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.

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.

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.

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

• FI = Langages fonctionnels et impératifs
• OX = Langages à objets et XML
• CO = Langages à contraintes