Wiki Agenda Contact Version française

Publications : Florian Faissole

Back
[9] 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, Amherst, MA, United States, June 2018. [ bib | full text on HAL ]
[8] Florian Faissole and Bas Spitters. Preuves constructives de programmes probabilistes. In Sylvie Boldo and Nicolas Magaud, editors, Vingt-neuvièmes Journées Francophones des Langages Applicatifs, Banyuls-sur-mer, France, January 2018. [ bib | full text on HAL ]
[7] Florian Faissole. Définir le fini : deux formalisations d'espaces de dimension finie. In Sylvie Boldo and Nicolas Magaud, editors, Vingt-neuvièmes Journées Francophones des Langages Applicatifs, Banyuls-sur-mer, France, January 2018. [ bib | full text on HAL | .pdf ]
[6] Florian Faissole. Formalization and closedness of finite dimensional subspaces. In SYNASC 2017 - 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, TimiÈ™oara, Romania, September 2017. [ bib | http | .pdf ]
Keywords: filters ; finite dimensional subspaces ; formalization of mathematics ; functional analysis ; formal proof ; Coq
[5] 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, London, United Kingdom, July 2017. [ bib | DOI | full text on HAL | .pdf ]
[4] 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, Montpellier, France, June 2017. [ bib | full text on HAL | .pdf ]
[3] 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 2017, pages 79--89, New York, NY, USA, January 2017. ACM. [ bib | DOI | full text on HAL | .pdf ]
[2] Florian Faissole and Bas Spitters. Synthetic topology in HoTT for probabilistic programming. In The Third International Workshop on Coq for Programming Languages (CoqPL 2017), Paris, France, January 2017. [ bib | full text on HAL ]
[1] Florian Faissole and Bas Spitters. Synthetic topology in homotopy type theory for probabilistic programming. PPS 2017 - Workshop on probabilistic programming semantics, January 2017. Poster. [ bib | full text on HAL ]

Back
This page was generated by bibtex2html.