Thesis of Victor Sannier

De la logique linéaire aux systèmes de types pour l'analyse de sensibilité et la vérification de la confidentialité différentielle

This thesis develops formal methods for verifying relational properties of probabilistic programs, primarily differential privacy. First, we define type systems inspired by linear logic to bound the sensitivity of functional programs and provide their denotational semantics in the category of metric spaces. Specifically, we address global sensitivity with respect to vector metrics, as well as local sensitivity, for which we introduce the concept of dependent coeffects. Second, we formalise the concurrent composition theorem for interactive differential privacy using session types within a probabilistic process calculus.

Jury

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.

Thesis of the team SyCoMoRES defended on 21/09/2026