08/11/2001: Alexandra Bruasse Bac (IML)
Logique Linéaire Indexée du Second Ordre

Résumé
Au cours de cet exposé, nous nous intéresserons à l'extension au second ordre de la logique linéaire indexée (LL(I)) définie par Bucciarelli et Ehrhard en 2000.
Puisque la base du système LL(I) est le modèle relationnel de la logique linéaire, notre première tâche consistera à définir un tel modèle pour la logique linéaire du second ordre. L'un des principaux "challenge" consistera en fait à définir une notion appropriée de composition des objets de type variable.
Dans ce modèle, les formules seront alors interprétées par des foncteurs stables (en un sens proche de celui de Girard pour le système F).
Sur ces bases, nous définirons alors les formules du système LL^2(I) et nous introduirons les opérations de restrictions, de relocalisation (une généralisation du renommage bijectif de LL(I)) et de substitution. Une fois cette trousse à outils prête, nous verrons alors que la relation existant entre LL^2(I) et le modèle relationnel de LL^2 est identique à celle qui existait pour LL.
Nous terminerons par un rapide tour de la sémantique des phases de LL^2(I) et nous verrons que cette dernière fournit en fait une sémantique dénotationnelle de LL^2, même si cette relation est plus "tortueuse" qu'elle ne l'était dans LL.