Ma soutenance

Investigating the expressivity of linear logic subsystems characterizing polynomial time

Jeudi 02 juillet 2015 à 13h30
Amphi B, Site Monod de l'ENS Lyon

Planning approximatif

Comment venir

Les différents lieux sont tous au site Monod de l'ENS Lyon. L'entrée dans le bâtiment se fait sous l'arche (croix clignotante).

La ligne B du métro relie directement la gare Part-Dieu à l'arrêt Debourg.

Contenu de la thèse

La version de la thèse envoyée au Jury se trouve ici. Résumé en français:

La complexité implicite est la caractérisation de classes de complexité par des restrictions syntaxiques sur des modèles de calcul. Plusieurs sous-systèmes de la logique linéaire caractérisant le temps polynomial ont été définis: ces systèmes sont corrects (les termes normalisent en temps polynomial) et complets (il est possible de simuler une machine de Turing pendant un nombre polynomial d'étapes).

Un des buts sur le long terme est de donner statiquement des bornes de complexité. C’est pourquoi nous cherchons les caractérisations du temps polynomial les plus expressives possible. Notre principal outil est la sémantique des contextes: des jetons voyagent à travers le réseau selon certaines règles. Les chemins définis par ces jetons représentent la réduction du réseau.

Contrairement aux travaux précédents, nous ne définissons pas directement des sous-systèmes de la logique linéaire. Nous définissons d'abord des relations -> sur les sous-termes des réseaux de preuves tel que: B -> C ssi ”le nombre de copies de B dépend du nombre de copies de C”. L’acyclicité de -> borne le nombre de copies de chaque sous-terme, donc la complexité du terme. Ensuite nous définissons des sous-systèmes de la logique linéaire assurant l’acyclicité de ->.

Nous étudions aussi des caractérisations du temps élémentaire et primitif récursif. Dans le but d’adapter nos sous-systèmes de la logique linéaire à des langages plus riches, nous adaptons la sémantique des contextes aux réseaux d’interaction, utilisés comme langage cible pour de petits langage de programmation. Nous utilisons cette sémantique des contexte pour définir une sémantique dénotationnelle sur les réseaux d’interactions.