<-- Back to the home page
Research interests
My research is about formalizing mathematics in the proof assistant Coq with the purpose of verifying numerical methods.
My work of formalization can be divided in several topics described bellow. For further reading see my publications and talks.
- Formalization of Newton's method and Kantorovitch's theorem
Newton's method is a simple numerical analysis algorithm used for approximating the roots of a given function.
Kantorovitch's theorem gives sufficient conditions for the convergence of Newton's method towards the root of the given function.
The theorem is expressed in the general case of a function of several variables.
My work consisted in formalising Kantorovitch's theorem in Coq.
The paper A Formal Verification of Kantorovitch's Theorem describes this formalisation.
- Formalization of multivariate analysis
The formalisation of multivariate analysis concepts in Coq was done using the ssreflect extension of the system and some libraries developed upon it in the Mathematical Components project.
The files describing the multivariate analysis concepts and the proof of Kantorovitch theorem in the multidimensional case are here and the paper is A Formal Verification of Kantorovitch's Theorem.
- Verification of exact computation with Newton's method
Together with Nicolas Julien we did some work on adapting Newton's method for exact real arithmetic with co-inductive streams. The page dedicated to this work is here .
- Formalization of interval analysis
My most recent work concerns interval analysis, in particular formalising proofs on regularity of interval matrices. Some files are available here .