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

Modèles des langages de programmation (48h, 6 ECTS)

Responsables : Thomas Ehrhard et Paul-André Melliès

Plan du cours et intervenants prévus pour 2019-2020

  1. Catégories et logique linéaire. (18h, Paul-André Melliès)
  2. Domaines, réalisabilité et lambda-calcul pur. (15h, Thomas Ehrhard)
  3. Sémantique des jeux et machines abstraites. (15h, Pierre-Louis Curien)

Objectifs

La filière introduira aux méthodes développées par la sémantique dénotationnelle pour décrire mathématiquement les langages de programmation fonctionnels, organisés autour d'un noyau de lambda-calcul. Le cours traitera des deux piliers du sujet: domaines de Scott et sémantique des jeux, et soulignera les points de convergence avec la théorie de la démonstration et la théorie des catégories.

Plan du cours

Catégories
Interprétation catégorique du λ-calcul et de la logique linéaire.
  • Catégories cartésiennes closes et λ-calcul simplement typé,
  • Catégories symétriques monoïdales closes et logique linéaire,
  • Catégories *-autonomes et dualité,
  • Monades, monoïdes et duplication,
  • Catégories de dialogue et logique tensorielle.
Modèles statiques
Principes et méthodes de la sémantique dénotationnelle.
  • Lambda-calcul et récursion: le langage PCF,
  • Domaines de Scott et continuité,
  • Domaines qualitatifs et stabilité,
  • Domaines qualitatifs avec cohérence et stabilité forte,
  • Domaines qualitatifs et espaces cohérents,
  • Relations logiques et écrasement extensionnel.
Modèles dynamiques
Sémantique des jeux et interprétation des programmes comme stratégies d'interaction.
  • Logique tensorielle et dualité entre Programme et Environnement,
  • Jeux d'arène (Hyland, Ong, Nickau) et jeux d'indices (Abramsky, Jagadeesan, Malacaria) pour PCF,
  • Correspondance syntaxe-sémantique : théorèmes de complétude forte,
  • PCF avec contrôle : interprétation de la logique classique,
  • PCF avec déclaration de variables locales : interprétation d'Algol Idéalisé,
  • Linéarité et parenthésage en sémantique des jeux,
  • Ludique.

Pré-requis

  • bases de calculabilité et récursivité,
  • bases de λ-calcul,
  • notions élémentaires de logique,
  • notions élémentaires de théorie des catégories.

Bibliographie

  • Paul-André Melliès. Categorical semantics of linear logic. Paru dans la série Panoramas et Synthèses, Société Mathématique Française, 2009.
  • Samson Abramsky and Guy McCusker. Games Semantics. In: Computational Logic, Proceedings of the 1997 Marktoberdorf Summer School, H. Schwichtenberg and U. Berger eds, Springer-Verlag, 1999.
  • Roberto Amadio and Pierre-Louis Curien. Domains and Lambda-Calculi. Cambridge University Press, 1998.
  • Martin Hyland. Game Semantics. In: Semantics and logics of computation, A. Pitts and P. Dybjer editors. Publications of the Newton Institute, Cambridge University Press, 1997.

Le calendrier des cours

Paul-André Melliès Cours 12 September
Cours 19 September
Cours 26 September
Cours 3 October
Cours 10 October
Cours 17 October
Cours 24 October
Cours 31 Octobre
Cours 7 November
Cours 14 November
Relâche 21 November
Examen partiel à partir de 8h45 28 November
Cours 5 December
Cours 12 December
Thomas Ehrhard Cours 19 December
Cours 9 January
Cours 16 January
Cours 23 January
Cours 30 January
Cours 6 February
Cours 13 February
Cours 20 February
Relâche 27 February
Examen Final à partir de 8h45 (salle 1013) 5 March

Équipe pédagogique

A. Bucciarelli MC Paris Diderot IRIF
J. Chroboczek MC Paris Diderot IRIF
P.-L. Curien DR CNRS IRIF
T. Ehrhard DR CNRS IRIF
C. Faggian CR CNRS IRIF
A. Guatto MdC Paris Diderot IRIF
G. Longo DR CNRS LIENS
D. Mazza CR CNRS LIPN
P.-A. Melliès DR CNRS IRIF
M. Pagani PR Paris Diderot IRIF
C. Tasson MC Paris Diderot IRIF

Vous trouverez ici les transparents et notes associés au cours.

 
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