## Phd student, Inria - Toccata / LRI - VALS

## Research

**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.

### Reports:

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

pdf.

### Posters:

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

### Talks:

**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.

## Enseignement

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.

## Bio

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**.

## Contact

Mail: prenom.nom@lri.fr

Address: Bureau 75,

LRI, Bâtiment 650,

Université Paris-Sud,

91405 ORSAY Cedex,

FRANCE.