Programme de l’UE

On étudiera les systèmes concurrents et le calcul fonctionnel par le biais de deux formalismes: les calculs de processus d’une part, et le lambda-calcul d’autre part. Des problèmes comparables se posent pour
l’analyse des systèmes dans les deux cadres: peut-on statiquement garantir que l’exécution d’un programme va terminer ? Peut-on apporter des bornes de complexité en temps sur cette terminaison?

Dans le cas des calculs concurrents, on développera les concepts permettant de raisonner sur la dynamique des systèmes, sur l’équivalence de processus, et sur leur terminaison. Dans celui du lambda-calcul on présentera des systèmes de types dérivés de la logique linéaire et permettant de garantir statiquement des bornes de complexité sur les programmes. On illustrera ainsi comment des techniques communes (typage) peuvent être exploitées à la fois dans le cadre concurrent et dans le cadre fonctionnel.  Enfin si le temps le permet on verra comment les méthodes développées pour la complexité dans le cadre du calcul fonctionnel inspirent des approches similaires dans le cadre concurrent.

Prérequis. 

  • notions élémentaires de lambda-calcul simplement typé,
  • définitions de base de classes de complexité en temps déterministe (les notions des cours d’algorithmique de L3 sont suffisantes). Les définitions nécessaires seront cependant rappelées.

Calendrier prévisionnel : 08/10, 09/10, 16/10, 22/10, 23/10, 6/11, 12/11, 13/11, 19/11, 26/11, 27/11, 4/12

Modalités d’examen. Un devoir à la maison en cours de trimestre, et un examen écrit à la fin du cours.

Intervenants:

  • Patrick Baillot, CR CNRS (responsable)
  • Damien Pous, CR CNRS