21 septembre 2026 à 14h (Bâtiment ESPRIT - Atrium)
Cette thèse développe des méthodes formelles pour vérifier les propriétés relationnelles des programmes probabilistes, principalement la confidentialité différentielle. Tout d’abord, nous définissons des systèmes de types inspirés de la logique linéaire afin de borner la sensibilité de programmes fonctionnels et nous en donnons une sémantique dénotationnelle dans la catégorie des espaces métriques. Plus précisément, nous considérons la sensibilité globale par rapport à des distances vectorielles, ainsi que la sensibilité locale, pour laquelle nous introduisons le concept de coeffets dépendants. Ensuite, nous formalisons le théorème de composition concurrente pour la confidentialité différentielle interactive à l’aide de types de session dans un calcul de processus probabiliste.
M. Patrick BAILLOT Directeur de recherche CNRS Directeur de thèse, M. Andrzej MURAWSKI Professeur Université d’Oxford Rapporteur, Mme Catuscia PALAMIDESSI Directeur de recherche INRIA Rapporteure, M. Michele PAGANI Professeur des universités École Normale Supérieure de Lyon Examinateur, Mme Delia KESNER Professeure des universités Université Paris Cité Examinatrice, M. Ugo DAL LAGO Professeur Université de Bologne Examinateur, M. Damiano MAZZA Directeur de recherche CNRS Examinateur, M. Marco GABOARDI Professeur Université de Boston Co-encadrant de thèse.
français
English