Inria Saclay - Toccata team
Laboratoire de Recherche en Informatique
VALS team My main research interest is round-off error analysis of numerical methods to solve ordinary differential equations, such as Runge-Kutta methods. I am refining the error bounds using stability properties of these methods and I am taking exceptional behaviors into account (overflow and underflow). Furthermore, I formalize the results in the Coq proof assistant to formally exhibit bounds on the round-off errors. I am a user of the Flocq library for floating-point arithmetic in Coq.
I am also interested in formally proving functional analysis results for the formal verification of numerical methods to solve partial differential equations (such as the finite element method). My main contributions are the formal proof of the Lax-Milgram Theorem and the closedness proof of finite dimensional subspaces of Hilbert spaces. Our basis is the Coquelicot library for real analysis in Coq.
In addition, I am interested in the use of proof assistants to represent programming languages and semantics. On one hand, I have worked on the formalization of probabilistic programs in Coq in a constructive way, using an approach mixing homotopy type theory and synthetic topology. On the other hand, I work on the formalization of high-level synthesis tools and techniques compiling C code to hardware description languages. More precisely, I formalize the behavior of directives asserting loop-carried dependencies between variables of the source programs.