Florian Faissole

Phd student, Inria - Toccata / LRI - VALS

Page en français


Computer arithmetic and numerical analysis: I'm interested in the study of roundoff errors in the implementation of numerical schemes with floating-point numbers, as Runge-Kutta methods for instance. Furthermore, I formalize these methods in the Coq proof assistant in order to formally exhibit bounds on the roundoff errors. For this purpose, I am using the Flocq library for floating-point arithmetic in Coq.

Formal proofs, functional analysis and integration theory: I'm a member of the ELFIC working group which is interested in the use of formal methods to verify some properties of the finite element method. This numerical method relies on an important mathematical theory. One of my main contribution is the formalization of these results in Coq: Hilbert spaces, Lax-Milgram's Theorem. We rely on the Coquelicot library for real analysis in Coq. See the code.

Homotopy type theory and probabilistic programming: Synthetic topology is a mathematical formalism in which the opens and continuous maps are first-class citizens. Encoding this formalism in homotopy type theory (HoTT library), we constructively formalize notions of measure theory and probabilistic programming with continuous datatypes. See the code.

Formalization of railway scenarios (old): During my internship at SIEMENS Mobility, I was interested in the automated translation of railway safety scenarios from natural language to a formal language. For this purpose, I made a first translation in an intermediate language written in JAVA, and hence I used JavaCC to compile such scenarios in the SCOLA formal language.

Accepted papers, reports and talks

Accepted papers:

[1] Round-off Error Analysis of Explicit One-Step Numerical Integration Methods (Sylvie Boldo, Alexandre Chapoutot & Florian Faissole), ARITH 2017.
[2] A Coq formal proof of the Lax-Milgram theorem (Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin & Micaela Mayero), CPP 2017.
[3] Synthetic topology in HoTT for probabilistic programming (Florian Faissole & Bas Spitters), CoqPL 2017.


Preuves formelles en analyse fonctionnelle (in french) (Florian Faissole), rapport de stage de M2 (2016) : pdf.


Synthetic topology in homotopy type theory for probabilistic programming (Florian Faissole & Bas Spitters), PPS 2017.


Topologie synthétique en théorie homotopique des types pour les programmes probabilistes (in french), LRI-VALS seminar (Orsay) 2017.
Preuve formelle du théorème de Lax-Milgram (in french), EJCIM 2017 (Lyon).
A Coq formal proof of the Lax-Milgram theorem, CPP 2017 (Paris).
Preuves formelles en analyse fonctionnelle (in french), master thesis defense.


I'm teaching practical works at Paris-Sud University:

CS Bachelor: Operating systems (webpage of the course).
CS Bachelor: Software Engineering Project (webpage of the course).

I'm interested in teaching and education issues and I'm convinced that classical methods are of interest. More particularly, I think that it should be a pity to abandon the teaching of latin and/or ancient greek.


2016 - today: Phd, Computer Science, Inria Saclay, Paris-Saclay University, supervisors: S. Boldo et A. Chapoutot.
08/2016 - 09/2016: Research internship, Aarhus University (Danemark), supervisor: B. Spitters.
03/2016 - 07/2016: Stage de recherche, Inria Saclay, supervisor: S. Boldo.
2015 - 2016: MSc, Computer Science (Computer Science Fundations and Software Engineering), Paris-Saclay University (highest honors).
2013-2016: ÉNSIIE Engineer.
06/2015 - 09/2015: Engineering internship, SIEMENS.
2013: BSc, Mathematics, Évry-Val-d'Essonne University.
2011 - 2013: CPGE MPSI/MP, Lycée Masséna.


Mail: prenom.nom@lri.fr

Address: Bureau 75,
LRI, Bâtiment 650,
Université Paris-Sud,
91405 ORSAY Cedex,