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

1. Catégories et logique linéaire, domaines de Scott, espaces de cohérence, jeux de dialogue. (18h, Paul-André Melliès)
2. Modèles quantitatifs, principes et méthodes de la sémantique dénotationnelle, espaces de cohérence probabilistes (18h, Thomas Ehrhard)
3. Lambda-calcul probabiliste, sémantique de l'appel-par-nom et de l'appel-par-valeur (12h, Guillaume Geoffroy)

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.

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érence,
• 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é,
• Comonades, comonoïdes et duplication,
• Catégories de dialogue et sémantique des jeux.

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,
• Théorème d'adéquation,
• Deuxième exemple: les espaces de cohérence probabilistes.

Modèles probabilistes et stratégies d'évalution

Sémantique dénotationnelle de l'appel-par-nom et de l'appel-par-valeur

• Espaces de cohérence probabilistes (rappels),
• Interprétation de PCF probabiliste en appel-par-nom et en appel-par-valeur,
• Théorème d’adéquation pour le langage PCF probabiliste,
• Espérance du temps de calcul et terminaison presque sûre.

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

• 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.