Disséquer les Sémantiques Dénotationnelles :

Du bien établi H* aux plus récents coeffets quantitatifs

Soutenu le 23 Octobre à 9h45

Manuscrit (disponible ici)

Résumé

À travers la résolution de deux problèmes ouverts bien différents, cette thèse présente quatre approches distinctes permettant d'observer finement et de classer des modèles dénotationnels.

Dans un premier temps, l'on s'intéressera au λ-calcul non typé et à sa théorie observationnelle H* (en appel de tête). Nous donnons une caractérisation, au sein d'une large classe de modèles du λ-calcul non typé, des modèles pleinement adéquats pour H*: un K-modèle extentionnel D est pleinement adéquat si et seulement s'il est hyperimmune, i.e., les chaines mal fondées d'éléments de D ne sont pas capturées par aucune fonction récursive. Nous allons présenter deux techniques permettant de prouver cette même caractérisation de deux manières indépendantes: l'une purement sémantique et l'autre purement syntaxique. La preuve sémantique consiste en l'utilisation d'un modèle syntaxique, les arbres de B\"ohm, et de propriétés d'approximation filtrant le plongement de ces derniers dans nos modèles. La preuve syntaxique consiste en l'utilisation de syntaxes sémantiques, les λ-calculs avec tests, qui transcrivent les propriétés internes des modèles à un niveau syntaxique.

Dans un second temps, l'on s'intéressera aux BsLL, qui sont des raffinements de la logique linéaire où les exponentielles sont paramétrées par les éléments d'un semi-anneau S. Ces semi-anneaux capturent une notion de coeffet, i.e., les hypothèses requises par un programme sur son contexte (accessibilité d'une ressource, prérequis sur une entrée...). Nous faisons ici la première analyse dénotationnelle de BsLL. En particulier, nous décrivons deux manières d'extraire de tels modèles. L'une est ``a priori'': il s'agit de choisir un semi-anneau S le long duquel on va stratifier l'exponentielle usuelle de la logique linéaire. L'autre est au contraire ``a posteriori'': elle montre qu'à un modèle de la logique linéaire est naturellement associé une sorte de semi-anneau sémantique résultant en une interprétation de BsLL.

Carte

Soutenance

Hall aux farines, Hall F, 5ème étage (accès par le hall E, allée paire, ascenseur F)

[Pot]

Bâtiment Sophie Germain, 8 place Aurélie Nemours salle 3052, 3ème étage.

Soirée

Informations à venir.