Publications : Florian Faissole
Back| [19] | Paul Geneau de Lamarlière, Guillaume Melquiond, and Florian Faissole. Slimmer formal proofs for mathematical libraries. In Int. Conf. on Computer Arithmetic, 2023. [ bib | full text on HAL ] |
| [18] | Paul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché, and Raphaël Rieu-Helft. Formally verified bounds on rounding errors in concrete implementations of logarithm-sum-exponential functions. Research Report 9531, Inria, 2023. [ bib | full text on HAL ] |
| [17] |
Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude
Marché, David Mentré, and Hiroaki Inoue.
Automated formal analysis of temporal properties of Ladder
programs.
International Journal on Software Tools for Technology
Transfer, 24(6):977--997, 2022.
[ bib |
DOI |
full text on HAL ]
Keywords: Ladder language for programming PLCs ; Timing charts ; Formal specification ; Deductive verification ; Why3 environment |
| [16] | Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq formalization of Lebesgue integration of nonnegative functions. Journal of Automated Reasoning, 66:175--213, 2022. [ bib | DOI | full text on HAL ] |
| [15] | Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, and Hiroaki Inoue. Formal analysis of Ladder programs using deductive verification. Research Report RR-9402, Inria, April 2021. [ bib | full text on HAL ] |
| [14] |
Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and
Micaela Mayero.
A Coq formalization of Lebesgue integration of nonnegative
functions.
Research Report RR-9401, Inria, France, 2021.
[ bib |
full text on HAL ]
Keywords: Lebesgue integration ; Measure theory ; Coq ; Formal proof ; Coq ; Preuve formelle ; Théorie de la mesure ; Intégrale de Lebesgue |
| [13] | Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, and Hiroaki Inoue. Automated verification of temporal properties of Ladder programs. In Formal Methods for Industrial Critical Systems, volume 12863 of Lecture Notes in Computer Science, pages 21--38, 2021. [ bib | DOI | full text on HAL ] |
| [12] | Florian Faissole. Formalisation en Coq des erreurs d'arrondi de méthodes de Runge-Kutta pour les systèmes matriciels. In AFADL 2019 - 18e journées Approches Formelles dans l'Assistance au Développement de Logiciels, Toulouse, France, June 2019. [ bib | full text on HAL ] |
| [11] | Sylvie Boldo, Florian Faissole, and Alexandre Chapoutot. Round-off error and exceptional behavior analysis of explicit Runge-Kutta methods. IEEE Transactions on Computers, 2019. [ bib | DOI | full text on HAL | .pdf ] |
| [10] | Florian Faissole. Formalisations d'analyses d'erreurs en analyse numérique et en arithmétique à virgule flottante. Thèse de doctorat, Université Paris Saclay, 2019. [ bib | full text on HAL ] |
| [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, Timisoara, 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.