Florian Faissole

Doctorant, Inria - Toccata / LRI - VALS

English version

Recherche

Arithmétique des ordinateurs et analyse numérique : Je m'intéresse aux erreurs d'arrondis induites par l'arithmétique à virgule flottante dans l'implémentation de schémas numériques classiques, comme les méthodes de Runge-Kutta. Par ailleurs, je formalise ces schémas dans l'assistant de preuves Coq afin d'exhiber formellement des bornes sur les erreurs d'arrondi. Pour ce faire, j'utilise la bibliothèque Flocq (arithmétique flottante en Coq).

Preuves formelles, analyse fonctionnelle et théorie de l'intégration : Je suis membre du groupe de travail ELFIC, qui s'intéresse à l'introduction de méthodes formelles pour la vérification de propriétés de la méthode des éléments finis. Cette méthode de résolution numérique pour les équations aux dérivées partielles repose sur une base mathématique pléthorique. L'une de mes principales contributions est la formalisation de ces résultats mathématiques en Coq: espaces de Hilbert, théorème de Lax-Milgram. Nous nous basons sur la bibliothèque d'analyse réelle Coquelicot. Voir le code.

Théorie homotopique des types et programmation probabiliste : La topologie synthétique est un formalisme mathématique dans lequel les ouverts et les applications continues sont les objets primitifs. En encodant ce formalisme dans la théorie homotopique des types (bibliothèque HoTT), nous formalisons de manière constructive des notions de programmation probabilistes avec des types continus. Voir le code.

Formalisation de scénarios ferroviaires (anciennement) : Lors d'un stage d'ingénieur chez SIEMENS Mobility, je me suis intéressé à la traduction automatique de scénarios de sécurité ferroviaire en langue naturelle vers un langage formel. Pour ce faire, j'ai fait une première traduction vers un langage intermédiaire écrit en JAVA, puis ai utilisé JavaCC pour compiler les scénarios vers le langage formel SCOLA.

Publications, rapports et présentations

Publications acceptées :

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

Rapports :

Preuves formelles en analyse fonctionnelle (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, Séminaire LRI-VALS (Orsay) 2017.
Preuve formelle du théorème de Lax-Milgram, EJCIM 2017 (Lyon).
A Coq formal proof of the Lax-Milgram theorem, CPP 2017 (Paris).
Preuves formelles en analyse fonctionnelle, soutenance de stage de M2.

Enseignement

Je suis chargé d'enseignement à l'Université Paris-Sud :

L3 Informatique: Systèmes d'Exploitation (Sujet DM, Page du cours).
L3 Informatique: Projet de Génie Logiciel (Page du cours).

Je suis très intéressé par les questions de méthode d'enseignement et d'éducation, et suis un défenseur de l'école classique. Je pense notamment que la disparition de l'enseignement du latin et/ou du grec ancien serait un dommage culturel important.

Biographie

2016 - aujourd'hui : Doctorat en Informatique, Inria Saclay, Université Paris-Saclay, sous la direction de S. Boldo et A. Chapoutot.
08/2016 - 09/2016 : Stage de recherche, Université d'Aarhus (Danemark), sous la direction de B. Spitters.
03/2016 - 07/2016 : Stage de recherche, Inria Saclay, sous la direction de S. Boldo.
2015 - 2016 : M2 FIIL (Fondements de l'Informatique et Ingénierie du Logiciel), Université Paris-Saclay (mention TB).
2013-2016 : Ingénieur diplômé de l'ÉNSIIE.
06/2015 - 09/2015 : Stage ingénieur R&D, SIEMENS.
2013 : L3 Mathématiques, Université d'Évry-Val-d'Essonne.
2011 - 2013: CPGE MPSI/MP, Lycée Masséna.
2011 : Baccalauréat S (mention TB).

Contact

Mail: prenom.nom@lri.fr

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