ValidationCC+examen
EnseignantLorenzo Tortorade Falco
Années

Syllabus

Vers la moitié des années ’80 du siècle dernier, lorsque grâce à la correspondance de Curry-Howard le domaine de recherche au carrefour entre l’informatique théorique et la théorie de la démonstration est en plein essor, Jean-Yves Girard introduit et étudie des modèles dénotationnels du système F. Il découvre alors un modèle très simple de F, les espaces cohérents, qui possèdent de remarquables propriétés de dualité, et que les connecteurs de la logique intuitionniste se décomposent au moyen d’opérations plus élémentaires dans ce modèle. Qui plus est, il s’avère que cette décomposition peut être internalisée par le biais de nouveaux connecteurs logiques : c’est ainsi qu’aparaît la Logique Linéaire, comme structure sous-jacente à “la” logique en général, et aux processus calculatoires. La Logique Linéaire est un puissant outil pour analyser et contrôler l’utilisation des ressources en logique et en informatique. Sa nature de structure sous-jacente à la logique a conduit les chercheurs à développer des techniques, des approches et des méthodes qui ont été appliquées dans bien d’autres domaines (théorie de la séquentialité, sémantique de Scott, lambda-calcul, sémantiques de jeux, analyse de la logique classique et de son contenu calculatoire, complexité implicite, vérification, etc.).

Le cours présentera quelques outils fondamentaux de la théorie de la démonstration de la Logique Linéaire. Ils seront introduits à partir des questions qui ont conduit à leur mise au point et on cherchera à mettre en valeur les perspectives écloses par leurs propriétés.

Sommaire

L’ordre dans lequel seront abordées les différentes notions, ainsi que le déroulement du cours, seront établis d’un commun accord avec les enseignants du cours Preuves et Programmes : outils classiques qui a lieu habituellement pendant le même semestre.

Partie I) Introduction

  • espaces cohérents et Logique Linéaire : bref aperçu de l’histoire de l’invention de la Logique Linéaire
  • la Logique Linéaire comme système logique : calcul des séquents, focalisation et renversement, polarisation, fragments remarquables.

Partie II) Réseaux de démonstration

  • le fragment multiplicatif : critères de correction, élimination des coupures, interprétation dans les modèles à trame
  • le fragment multiplicatif et exponentiel : critères de correction, interprétation dans les modèles à trame, confluence, normalisation forte (preuve syntaxique et preuve sémantique)
  • les quantificateurs dans les réseaux
  • le système complet de réseaux pour la Logique Linéaire du second ordre
  • la question de la séparation dans les réseaux : comportement du modèle cohérent et du modèle relationnel
  • la Logique Linéaire différentielle comme raffinement de la Logique Linéaire : réseaux différentiels, expansion de Taylor d’un réseau de démonstration
  • inversion de la formule de Taylor et usage des réseaux différentiels pour séparer les comportements interactifs différents des réseaux de démonstration.

Partie III) Deux exemples d’usage de la Logique Linéaire en théorie de la démonstration

  • la Logique Linéaire comme outil pour extraire le contenu calculatoire des preuves classiques : intérêt et enjeux de l’extension de la correspondance de Curry-Howard à la logique classique, la méthode des décorations de Danos-Joinet-Schellinx, plongements de la logique classique dans la Logique Linéaire
  • un point de vue logique sur le temps borné : la méthode de Girard dans la recherche d’un système logique avec élimination des coupures en temps intrinsèquement borné, la Logique Linéaire élémentaire ELL et la Logique Linéaire Légère LLL/SLL, caractérisations syntaxiques et sémantiques du temps borné

Bibliographie

• Handbook of Linear Logic (available at he address: https://ll-handbook.frama.io/ll-handbook/main.pdf)
• J.-Y. Girard : Linear Logic (Theoretical Computer Science, Vol 50, no 1, pp. 1–102, 1987)
• J.Y. Girard, Y. Lafont, P. Taylor: Proofs and Types (Cambridge University Press, 1989)