Phd student.

List of publications

International conferences

[1 Sylvie Boldo, Florian Faissole, and Vincent Tourneur. A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers . In 25th IEEE Symposium on Computer Arithmetic, ARITH, Ahmerst, United States of America, July 2018. .pdf 
[2 Florian Faissole. Formalization and closedness of finite dimensional subspaces. In SYNASC 2017 - 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pages 1-7, Timişoara, Romania, September 2017, .pdf 
[3 Sylvie Boldo, Florian Faissole, and Alexandre Chapoutot. Round-off Error Analysis of Explicit One-Step Numerical Integration Methods. In 24th IEEE Symposium on Computer Arithmetic, ARITH, pages 82-89, London, United Kingdom, July 2017. .pdf 
[4 Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq Formal Proof of the Lax-Milgram theorem. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP, pages 79-89, Paris, France, January 2017. ACM. .pdf 

International workshops

[5 Florian Faissole, and Bas Spitters. Synthetic topology in homotopy type theory for probabilistic programming. In The Third International Workshop on Coq for Programming Languages, CoqPL, pages 1-2, Paris, France, January 2017.

National conferences

[6 Florian Faissole, and Bas Spitters. Preuves constructives de programmes probabilistes. In 29èmes journées Francophones des Langages Applicatifs, pages 137-150, Banyuls-sur-Mer, France, January 2018.
[7 Florian Faissole. Définir le fini: deux formalisations d'espaces de dimension finie. In 29èmes journées Francophones des Langages Applicatifs, pages 167-172, Banyuls-sur-Mer, France, January 2018. .pdf 
[8 Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. Preuve formelle du théorème de Lax-Milgram. In 16èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels, pages 1-2, Montpellier, France, June 2017. .pdf