Name
Henri Saudubray - PhD student
Synopsis
I am a PhD student at Laboratoire Méthodes Formelles (LMF) at
Université Paris-Saclay, focusing on formal logic, proof
assistants, and programming languages.
Publications
-
"Faire chauffer Why3 avec de l'induction".
Describes the addition of a new construct to the WhyML language allowing for case analysis on inductive predicate instances.
Written with Jean-Christophe Filliâtre and Andrei Paskevich.
Experience
-
Laboratoire Méthodes Formelles, Université Paris-Saclay - Since October 2025PhD, with Jean-Christophe Filliâtre and Andrei Paskevich. Working on the design and unification of programming, specification and proof languages in the context of deductive program verification, in the Why3 platform.INRIA, PARKAS Team - March to August 2025M2 Internship, with Marc Pouzet. Worked on reproducibility and transparency of assertions in the synchronous hybrid language Zélus. Designed and implemented a formal executable semantics for a multi-solver language runtime.Laboratoire Méthodes Formelles, CNRS - March to July 2024M1 Internship, with Jean-Christophe Filliâtre and Andrei Paskevich. Added support for case analysis and proofs by induction on inductive predicates in the Why3 platform. Translated a Coq proof to Why3 as a test.Skapánê - September 2022 to August 2023L3 Traineeship. Back-end development on containerized infrastructure in Python. Web app design with React.js, Flask and Docker.Informatique CDC - May to August 2022L2 Internship. Development of an automated end-to-end testing tool and ISO 20022 file format converter for CDC's banking infrastructure in Java.Ac'Lab - August 2021 - May 2022Association. Vice-Treasurer and Teaching Lead.Fnac Darty - May to August 2021L1 Internship. Work on customer insight and customer journey. Deployment of an in-house iOS application.Education
-
ENS Paris-Saclay - September 2024 - March 2025Master Parisien de Recherche en Informatique (MPRI)
-
Faculté des Sciences - Université Paris-Saclay - September 2023 - March 2024Master Parisien de Recherche en Informatique (MPRI)
-
FGES - Université Catholique de Lille - September 2020 to May 2023Licence Sciences du Numérique (SDN)
Files-
Curriculum Vitae.
-
Report for M1 Internship.
-
Report for M2 Internship.
See Also-
Email address.
-
Git forge.
-
LinkedIn.