Name
Maïga 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.
Teaching
-
Introduction to Computer Science, L1 Informatique, UFR Sciences, Université Paris-Saclay - October 2025 to January 2026TA. Introduction to Computer Science: Python, HTML/CSS, networks basics.
-
Introduction to Deductive Verification, PEIP2, Polytech Paris-Saclay - December 2025 to January 2026TA. Introduction to Deductive Verification with Why3.
-
Object-oriented Programming and Software Engineering, L2 Informatique, UFR Sciences, Université Paris-Saclay - January to April 2026TA. UML, Java, object-oriented design patterns.
-
Databases, PEIP2, Polytech Paris-Saclay - March to April 2026TA. Introduction to SQL, pandas.
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.OCaml Users in PariS - Since September 2025Seminar organisation. Presentations around the OCaml programming language and its uses both in academic and professional contexts.LMF Non-Permanent Members Seminar - Since May 2026Seminar organisation. Scientific presentations by and for the Laboratoire Méthodes Formelles's non-permanent members.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.