La soutenance aura lieu devant le jury suivant :

1. Frédérique Bassino, (LIPN, Université Paris 13)
2. François Bergeron, (UQAM, Université du Québec à Montreal)
3. Jean-Marc Fédou, (I3S, Université de Nice Sophia-Antipolis)
4. Vlady Ravelomanana, (IRIF, Université Paris Diderot)
5. Bruno Salvy, (LIP, ENS Lyon)
6. Michèle Soria, (LIP6, Université Paris 6)

après avis des rapporteuses :

1. Marilena Barnabei, (Dipartimento di Matematica, Università di Bologna)
2. Frédérique Bassino, (LIPN, Université Paris 13)
3. Valérie Berthé, (IRIF, Université Paris Diderot)

Depuis les années 60, la sémantique s'est avérée très utile pour introduire des langages de haut niveau permettant d'écrire des programmes complexes et de les comprendre à un niveau mathématique précis. Dans les années 80, la logique linéaire a été introduite par Girard, reflétant des propriétés sémantiques liées à l'utilisation des ressources. Cette direction a été poursuivie par Ehrhard dans les années 2000 avec l'introduction du lambda-calcul différentiel. Dans ces modèles, les programmes sont approximés par des polynômes, dont les monômes représentent les appels d'un programme à ses entrées lors de son exécution. Cette approche analytique a constitué un outil crucial pour l'étude des propriétés quantitatives apparaissant dans les langages de programmation probabiliste. En parallèle, depuis les années 90, plusieurs modèles géométriques ont été développés pour représenter des traces d'exécution dans les systèmes distribués. Dans cette thèse d'habilitation, nous présentons des modèles que nous avons étudiés dans ces trois domaines : les systèmes distribués, le lambda-calcul différentiel, la programmation probabiliste, ainsi que les techniques générales nécessaires et les résultats qu'ils nous ont permis d'obtenir. Celles-ci ont nécessité l'utilisation et le développement d'outils issus de la combinatoire, de la topologie dirigée, de l'analyse fonctionnelle, de la théorie des catégories et des probabilités.

https://upsilon.cc/~zack/research/hdr/

La logique tensorielle est une logique primitive du tenseur et de la négation, dont l'objectif est de circonscrire les ingrédients élémentaires du raisonnement logique, et de les étudier au moyen des outils de l'algèbre contemporaine.

La logique est aussi conçue pour fonder la sémantique des jeux en théorie des types, et pour l'articuler de manière précise et harmonieuse avec la logique linéaire et la théorie des continuations dans les langages de programmation.

https://www.irif.fr/~mellies/habilitation.html