[TYPES/announce] Two fully-funded PhD positions in France on formal verification of probabilistic programs and differential privacy

[Martin Avanzini]

We are offering two fully-funded PhD positions in the context of the ANR project HOPR (Higher-Order Probabilistic and resource-aware Reasoning; ANR-24-CE48-5521-01). Broadly, HOPR's aim lies in defining expressive logical frameworks, dealing in particular with higher-order computation and probabilities, which can serve to reason on cryptographic primitives and protocols and on differential privacy. The project, coordinated by Patrick Baillot, has four partner sites: INRIA Lille/CRIStAL; INRIA Paris; IRISA Rennes and INRIA Sophia-Antipolis. It started in January 2025 for a duration of 4 years.

Specifically, we are offering:
- one position at INRIA Lille/CRIStAL, supervised by Patrick Baillot, on "Verification of Differential Privacy", see https://urldefense.com/v3/__https://jobs.inria.fr/public/classic/en/offres/2024-08486__;!!IBzWLUs!VqZ2YRUOuPzrvfk2S87wHhr5RawrYHX_a1dqLtFXSe-2QgBdXPF36p7Cti2tAxccrVmBDvXu6r91mZfEKtwKQP5TNx0oeotx08HuLd8vFg$  ; and
- one position at INRIA Sophia-Antipolis, supervised by Martin Avanzini and Benjamin Gregoire, on "Verification of Higher-Order, Probabilistic Programs", see https://urldefense.com/v3/__https://recrutement.inria.fr/public/classic/en/offres/2025-08539__;!!IBzWLUs!VqZ2YRUOuPzrvfk2S87wHhr5RawrYHX_a1dqLtFXSe-2QgBdXPF36p7Cti2tAxccrVmBDvXu6r91mZfEKtwKQP5TNx0oeotx08GtEQHu2g$  .

Positions should start no later than October 2025. Interested candidates are encouraged to apply following the above links.

We would greatly appreciate it if you could share this opportunity with your students or anyone interested in pursuing research on the advertised topics. Feel free to contact us (patrick.baillot at univ-lille.fr or martin.avanzini at inria.fr) if you have any additional questions.