Maître de Conférences (Associate Professor)
UPS / IRIT2 / Level 4, Office: 473
+33 (0)5 61 55 6416
The following keywords recap my main research interests:
- formal methods: formal proof assistants (Coq, SSReflect, PVS), formalization of mathematics, type theory, proof theory, classical and intuitionnistic logics, formal specifications, formal verification, certificates;
- numerical methods: computer arithmetic, floating-point arithmetic, correct rounding, certified polynomial approximation, interval arithmetic, global optimization, computer algebra;
- game theory: formal proof for game theory: formalization of Boolean games, determinacy, games in normal form...
- software engineering : CI/CD, automating tests, V&V or continuous deployment...
Current Research Activities
My research activities focus on the applications of interactive formal proof, in particular for the formal verification of results in computer arithmetic and game theory.
I am also interested in designing methods to increase proof automation within formal proof assistants, as well as automating tests in general and specifically around the tooling of projects in the OCaml and Coq community.
Since the 1st September 2014, I am Associate Professor (Maître de Conférences) at the Université Toulouse III – Paul Sabatier and I do my research in the ACADIE team of the IRIT research lab.
Previously, I was a postdoc in the VALS/Toccata team of LRI (UMR 8623 CNRS & Université Paris-Sud) at Inria Saclay - Île-de-France and was involved in the VERASCO project of the French ANR.
Before that, I was a postdoc in the Marelle project-team at Inria Sophia Antipolis, and was involved in the TaMaDi project of the French ANR.
I defended my PhD thesis on the 26th September 2012 in ENS de Lyon, where I worked in the AriC project-team (formerly known as Arénaire) of the LIP research laboratory, under the joint supervision of Jean-Michel Muller and Micaela Mayero.
My PhD manuscript and my PhD defense slides are available online.
Certified, Efficient and Sharp Univariate Taylor Models in COQ
at SYNASC 2013.
Formal proofs and certified computation in Coq
at Games 2015.
Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq
at FAC 2016.
A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations
at CPP 2017.
An Existence Theorem of Nash Equilibrium in Coq and Isabelle
at GandALF 2017 (code).
The under tactic (math-comp meeting, 2019-02-28)
SSReflect in Coq 8.10 at the Coq Workshop 2019 (Demo)
Primitive Floats in Coq at ITP 2019
Overview of the recent and upcoming features of Learn-OCaml (Learn-OCaml WG, 2022-03-23)
Learn-OCaml: How to contribute? (Learn-OCaml WG, 2022-03-23)
Overview of the PFITAXEL project Using the Learn-OCaml platform (DAS e-education@IRIT, 2022-05-20)
Learn-OCaml Presentation (in French) at the 1st Meetup Toulouse OCaml UserS (2022-10-11)
Hardware floating-point computations in Coq at Certified and Symbolic-Numeric Computation (ENS de Lyon, 2023-05-26)
Internship proposals (2022-2023)
If you are strongly interested in one of the research topics that I mention, but no internship proposal about it appears at the time, feel free to contact me and send me a CV+cover-letter, to discuss a possible internship supervised by me within the ACADIE team.
Supervision of PhD students
Co-advisor (with Hélène Fargier) of the PhD thesis of Pierre Pomeret-Coquot (2020-2023, MESR/ED-MITT grant)
||In particular, I belong to the steering committee of the Master DL for which I do most of my teaching activities.
More precisely, I have been involved in the following teaching units (in reverse chronological order):
« TD/TP d'Algorithmique et Programmation procédurale
– LIF5 (niveau L2) »
with Samir Akkouche
« TD d'Architecture matérielle et logicielle
– LIF6 (niveau L2) »
with Nicolas Louvet
« TP d'Algorithmique, Programmation et Complexité
– LIF9 (niveau L3) »
with Julien Mille
and Ricardo Uribe Lobello
« TD de Preuve assistée par ordinateur
avec Coq (niveau M1) »
with Jean Duprat
and Aurélien Pardon
at ENS de Lyon.
« TP de Programmation fonctionnelle et récursive en Scheme
– LIF3 (niveau L1) »
with Nathalie Guin
« TP d'Algorithmique et programmation impérative
– LIF1 (niveau L1) »
with Élodie Desseree