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

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)

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

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