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

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)

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.

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.

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