RESSOURCES EN LIGNE ET ACTUALITÉS
SCIENTIFIQUES FRANCOPHONES

3237 - Logique linéaire indexée du second ordre

Description bibliographique

Auteur :

Bac-Bruasse, Alexandra (Université de la Méditerranée, Aix-Marseille 2. IML. Institut de mathématiques de Luminy. France) ; Girard, Jean-Yves (dir.) ; Ehrhard, Thomas (dir.)

Éditeur :

Université de la Méditerranée, Aix-Marseille 2. IML. Institut de mathématiques de Luminy. France

Page source :

Thèses de l'IML, http://iml.univ-mrs.fr/theses/

Langue :

français

Diplôme :

Thèse, Mathématiques, Logique de la programmation, 2001/12/18

Description du contenu

Spécialité :

Sciences exactes - Mathématiques - Logique et fondements mathématiques

Mots clés :

sémantique dénotationnelle ; sémantique des phases ; logique linéaire indexée

Table des matières :

Introduction
1 - Pour poser le décor
2 - Le système LL^2(I)
3 - Modèles dénotationnels non uniformes de LL^2(I)
4 - Le modèle relationnel de LL^2(I)
5 - La logique linéaire indexée du second ordre
6 - La sémantique des phases de LL^2(I)
Bibliographie
Annexe 1 - Quelques rappels catégoriques
Annexe 2 - Caml dans les faits
Index

Résumé :

Le but de cette thèse est d'étendre au second ordre la logique linéaire indexée introduite en 1999-2000 par Bucciarelli et Ehrhard. L'une des motivations de ce travail est que, le traitement sémantique des unités restant insatisfaisant, il est souhaitable qu'on puisse utiliser des variables propositionnelles. La première étape de ce travail consiste à définir un modèle relationnel de la logique linéaire du second ordre. On peut alors construire un système appelé logique linéaire indexée du second ordre et noté $LL^2(I)$. Nous nous penchons ensuite sur la définition d'une sémantique des phases pour $LL^2(I)$. Tout comme dans la logique linéaire indexée, cette dernière n'est pas complète, mais on peut construire une extension de $LL^2(I)$ pour laquelle la complétude est atteinte. A partir de chaque modèle de phases, on obtient un modèle dénotationnel non uniforme de $LL^2$ et on peut, par exemple, définir des espaces cohérents non uniformes pour la logique linéaire du second ordre. (d'après résumé d'auteur)

Accès à la ressource

Format :

PDF
Taille du fichier : entre 1 et 2 Mo

Notes :

Document de 199 pages.

URL de référence :

http://iml.univ-mrs.fr/theses/files/TheseBac.pdf

Ressource copiée dans le cache de l'Infothèque le 08/08/2007

URL de référence :

/cache/3237/iml.univ-mrs.fr/theses/files/TheseBac.pdf

Notice mise en ligne le 28/02/2003 et mise à jour le 07/08/2007