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 2020 - 2021

  1. Catégories et logique linéaire, domaines de Scott et espaces de cohérence. (16h, Paul-André Melliès)
  2. Modèles quantitatifs, principes et méthodes de la sémantique dénotationnelle, lambda-calcul probabiliste (16h, Thomas Ehrhard)
  3. Machines abstraites, correspondances entre sémantique dénotationnelle et opérationnelle, espérance de temps de calcul (16h, Michele Pagani)

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. En plus du lien avec la théorie des catégories, le cours traitera des deux piliers du sujet: sémantiques qualitatives et quantitatives issues des domaines de Scott et de la logique linéaire, ainsi que leur correspondance avec des propriétés opérationnelles des langages de programmation aussi bien déterministes que probabilistes.

Plan du cours

Logique linéaire et catégories
Interprétation catégorique du λ-calcul et de la logique linéaire.
  • Domaines de Scott et espaces de cohérences
  • 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 quantitatifs et logique linéaire
Principes et méthodes de la sémantique dénotationnelle.
  • Lambda-calcul et récursion: le langage PCF,
  • Modèles de la logique linéaire: catégories de Seely,
  • Premier exemple: ensembles et relations,
  • Le modèle relationnel de PCF, types intersection non-idempotents,
  • Deuxième exemple: les espaces cohérents probabilistes.
Modèles quantitatifs et machines abstraites
Correspondances entre sémantique dénotationnelle et opérationnelle.
  • Machine abstraite de Krivine pour le langage PCF,
  • Temps de calcul dans le modèle déterministe et modèles quantitatifs,
  • Espaces cohérents probabilistes (rappels),
  • Théorème d’adéquation pour le langage PCF probabiliste,
  • Espérance du temps de calcul et terminaison presque sûre.

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.
  • Roberto Amadio and Pierre-Louis Curien. Domains and Lambda-Calculi. Cambridge University Press, 1998.
  • Jean-Yves Girard. Linear Logic. Theoretical Computer Science, 1987.
  • Gordon Plotkin. LCF considered as a programming language. Theoretical Computer Science, 1977.
  • Thomas Ehrhard, Michele Pagani and Christine Tasson. Full Abstraction for Probabilistic PCF. Journal of the ACM, 2018.
  • 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 15 September
Cours 22 September
Cours 29 September
Cours 3 October
Cours 6 October
Cours 13 October
Cours 20 October
Cours 27 October
Cours 3 November
Thomas Ehrhard Cours 10 November
Cours 17 November
Relâche 24 November
Examen partiel à partir de 8h45 1 December
Cours 8 December
Cours 15 December
Cours 5 January
Cours 12 January
Cours 19 January
Michele Pagani Cours 26 January
Cours 2 February
Cours 9 February
Cours 16 February
Cours 23 February
Relâche 2 March
Examen Final à partir de 8h45 (salle 1013) 9 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 MC Paris Diderot IRIF
D. Mazza DR CNRS LIPN
P.-A. Melliès DR CNRS IRIF
M. Pagani PR Paris Diderot IRIF
D. Petrisan MC Paris Diderot IRIF
C. Tasson PR Sorbonne Université

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