faissole.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc faissole.cite -ob faissole.bib -c 'author : "faissole"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@inproceedings{boldo:hal-01391578,
topics = {team},
title = {{A Coq Formal Proof of the Lax-Milgram theorem}},
author = {Boldo, Sylvie and Cl{\'e}ment, Fran\c{c}ois and Faissole, Florian
and Martin, Vincent and Mayero, Micaela},
hal = {https://hal.inria.fr/hal-01391578},
booktitle = {{Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs}},
series = {CPP 2017},
location = {Paris, France},
year = {2017},
month = jan,
pages = {79--89},
pdf = {https://hal.inria.fr/hal-01391578/file/article.pdf},
doi = {10.1145/3018610.3018625},
publisher = {ACM},
address = {New York, NY, USA}
}
@inproceedings{boldo17arith,
topics = {team},
title = {Round-off Error Analysis of Explicit One-Step Numerical Integration Methods},
author = {Boldo, Sylvie and Faissole, Florian and Chapoutot, Alexandre},
hal = {https://hal.archives-ouvertes.fr/hal-01581794},
booktitle = {24th IEEE Symposium on Computer Arithmetic},
address = {London, United Kingdom},
year = {2017},
month = jul,
doi = {10.1109/ARITH.2017.22},
pdf = {https://hal.archives-ouvertes.fr/hal-01581794/file/arith_hal.pdf}
}
@inproceedings{BCF17b,
topics = {team},
title = {Preuve formelle du th{\'e}or{\`e}me de {Lax--Milgram}},
author = {Boldo, Sylvie and Cl{\'e}ment, Fran\c{c}ois and Faissole, Florian and Martin, Vincent and Mayero, Micaela},
hal = {https://hal.archives-ouvertes.fr/hal-01581807},
booktitle = {{16{\`e}mes journ{\'e}es Approches Formelles dans l'Assistance au D{\'e}veloppement de Logiciels}},
address = {Montpellier, France},
year = {2017},
month = jun,
pdf = {https://hal.archives-ouvertes.fr/hal-01581807/file/article_afadl.pdf}
}
@inproceedings{Faissole17,
topics = {team},
title = {{Formalization and closedness of finite dimensional subspaces}},
author = {Faissole, Florian},
url = {https://hal.inria.fr/hal-01630411},
booktitle = {{SYNASC 2017 - 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing}},
address = {Timisoara, Romania},
year = {2017},
month = sep,
keywords = {filters ; finite dimensional subspaces ; formalization of mathematics ; functional analysis ; formal proof ; Coq},
pdf = {https://hal.inria.fr/hal-01630411/file/synasc_hal.pdf},
hal_id = {hal-01630411},
hal_version = {v1}
}
@inproceedings{spitters18jfla,
topics = {team},
crossref = {jfla18},
title = {Preuves constructives de programmes probabilistes},
author = {Faissole, Florian and Spitters, Bas},
hal = {https://hal.inria.fr/hal-01654459},
hal_id = {hal-01654459},
hal_version = {v1}
}
@inproceedings{faissole18jfla,
topics = {team},
crossref = {jfla18},
title = {D{\'e}finir le fini : deux formalisations d'espaces de dimension finie},
author = {Faissole, Florian},
hal = {https://hal.inria.fr/hal-01654457},
pdf = {https://hal.inria.fr/hal-01654457/file/jfla.pdf},
hal_id = {hal-01654457},
hal_version = {v1}
}
@inproceedings{boldo18arith,
topics = {team},
title = {A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers},
author = {Boldo, Sylvie and Faissole, Florian and Tourneur, Vincent},
hal = {https://hal.inria.fr/hal-01772272},
booktitle = {25th IEEE Symposium on Computer Arithmetic},
address = {Amherst, MA, United States},
year = 2018,
month = jun
}
@inproceedings{faissole:hal-01405762,
topics = {team},
title = {Synthetic topology in {HoTT} for probabilistic programming},
author = {Faissole, Florian and Spitters, Bas},
booktitle = {The Third International Workshop on Coq for Programming Languages (CoqPL 2017)},
address = {Paris, France},
year = 2017,
month = jan,
hal = {https://hal.inria.fr/hal-01405762}
}
@misc{faissole:hal-01485397,
topics = {team},
title = {Synthetic topology in homotopy type theory for probabilistic programming},
author = {Faissole, Florian and Spitters, Bas},
howpublished = {PPS 2017 - Workshop on probabilistic programming semantics },
year = 2017,
month = jan,
hal = {https://hal.inria.fr/hal-01485397},
note = {Poster}
}
@article{boldo19toc,
topics = {team},
title = {Round-off error and exceptional behavior analysis of explicit {Runge-Kutta} methods},
author = {Boldo, Sylvie and Faissole, Florian and Chapoutot, Alexandre},
hal = {https://hal.archives-ouvertes.fr/hal-01883843},
journal = {IEEE Transactions on Computers},
publisher = {Institute of Electrical and Electronics Engineers},
year = 2019,
doi = {10.1109/TC.2019.2917902},
pdf = {https://hal.archives-ouvertes.fr/hal-01883843/file/article_hal.pdf}
}
@inproceedings{faissole19afadl,
topics = {team},
title = {{Formalisation en Coq des erreurs d'arrondi de m{\'e}thodes de Runge-Kutta pour les syst{\`e}mes matriciels}},
author = {Faissole, Florian},
hal = {https://hal.archives-ouvertes.fr/hal-02391924},
booktitle = {AFADL 2019 - 18e journ{\'e}es Approches Formelles dans l'Assistance au D{\'e}veloppement de Logiciels},
address = {Toulouse, France},
year = 2019,
month = jun
}
@techreport{belo21rr,
topics = {team},
title = {Formal Analysis of {Ladder} Programs using Deductive Verification},
author = {Belo Louren\c{c}o, Cl{\'a}udio and Cousineau, Denis and Faissole, Florian and March{\'e}, Claude and Mentr{\'e}, David and Inoue, Hiroaki},
hal = {https://hal.inria.fr/hal-03199464},
type = {Research Report},
number = {RR-9402},
institution = {Inria},
year = 2021,
month = apr
}
@techreport{boldo21rr,
topics = {team},
title = {A {Coq} Formalization of {Lebesgue} Integration of Nonnegative Functions},
author = {Boldo, Sylvie and Cl{\'e}ment, Fran\c{c}ois and Faissole, Florian and Martin, Vincent and Mayero, Micaela},
hal = {https://hal.inria.fr/hal-03194113},
type = {Research Report},
number = {RR-9401},
institution = {Inria, France},
year = 2021,
keywords = {Lebesgue integration ; Measure theory ; Coq ; Formal proof ; Coq ; Preuve formelle ; Th{\'e}orie de la mesure ; Int{\'e}grale de Lebesgue}
}
@inproceedings{belo21fmics,
topics = {team},
title = {Automated Verification of Temporal Properties of {Ladder} Programs},
author = {Belo Louren{\c c}o, Cl{\'a}udio and Cousineau, Denis and Faissole, Florian and March{\'e}, Claude and Mentr{\'e}, David and Inoue, Hiroaki},
hal = {https://hal.inria.fr/hal-03281580},
booktitle = {Formal Methods for Industrial Critical Systems},
doi = {10.1007/978-3-030-85248-1_2},
series = {Lecture Notes in Computer Science},
volume = 12863,
pages = {21--38},
year = 2021
}
@phdthesis{faissole19phd,
topics = {team},
title = {Formalisations d'analyses d'erreurs en analyse num{\'e}rique et en arithm{\'e}tique {\`a} virgule flottante},
author = {Faissole, Florian},
hal = {https://tel.archives-ouvertes.fr/tel-02470728},
number = {2019SACLS594},
school = {Universit{\'e} Paris Saclay},
year = 2019,
type = {Th{\`e}se de Doctorat}
}
@article{belo22sttt,
topics = {team},
title = {Automated Formal Analysis of Temporal Properties of {Ladder} Programs},
author = {Belo Louren{\c c}o, Cl{\'a}udio and Cousineau, Denis and Faissole, Florian and March{\'e}, Claude and Mentr{\'e}, David and Inoue, Hiroaki},
hal = {https://hal.inria.fr/hal-03737869},
journal = {International Journal on Software Tools for Technology Transfer},
publisher = {Springer},
year = 2022,
pages = {977--997},
volume = 24,
number = 6,
doi = {10.1007/s10009-022-00680-0},
keywords = {Ladder language for programming PLCs ; Timing charts ; Formal specification ; Deductive verification ; Why3 environment}
}
@article{boldo22jar,
topics = {team},
title = {A {Coq} Formalization of {Lebesgue} Integration of Nonnegative Functions},
author = {Boldo, Sylvie and Cl{\'e}ment, Fran{\c c}ois and Faissole, Florian and Martin, Vincent and Mayero, Micaela},
hal = {https://hal.inria.fr/hal-03471095},
journal = {Journal of Automated Reasoning},
publisher = {Springer},
volume = 66,
pages = {175--213},
year = 2022,
doi = {10.1007/s10817-021-09612-0}
}
@inproceedings{geneau23arith,
topics = {team},
author = {Geneau de Lamarli{\`e}re, Paul and Melquiond, Guillaume and Faissole, Florian},
title = {Slimmer Formal Proofs for Mathematical Libraries},
hal = {https://inria.hal.science/hal-04165169},
booktitle = {Int. Conf. on Computer Arithmetic},
year = 2023
}
@techreport{bonnot23rr,
topics = {team},
author = {Bonnot, Paul and Boyer, Beno\^it and Faissole, Florian and March\'e, Claude and
Rieu-Helft, Rapha\"el},
title = {Formally Verified Bounds on Rounding Errors in Concrete Implementations of Logarithm-Sum-Exponential Functions},
institution = {Inria},
type = {Research Report},
number = 9531,
year = 2023,
hal = {https://inria.hal.science/hal-04343157}
}
@inproceedings{bonnot24fmcad,
topics = {team},
title = {Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function},
author = {Bonnot, Paul and Boyer, Beno{\^i}t and Faissole, Florian and March{\'e}, Claude and Rieu-Helft, Rapha{\"e}l},
hal = {https://inria.hal.science/hal-04674600},
booktitle = {Formal Methods in Computer-Aided Design},
publisher = {IEEE},
year = 2024
}
@inproceedings{faissole24itp,
topics = {team},
title = {End-to-End Formal Verification of a Fast and Accurate Floating-Point Approximation},
author = {Faissole, Florian and Geneau de Lamarli{\`e}re, Paul and Melquiond, Guillaume},
hal = {https://hal.science/hal-04515714},
booktitle = {5th International Conference on Interactive Theorem
Proving},
publisher = {Leibniz International Proceedings in Informatics},
address = {Tbilisi, Georgia},
volume = 309,
pages = {14:1-14:18},
year = 2024,
doi = {10.4230/LIPIcs.ITP.2024.14}
}
@techreport{bonnot24rr,
topics = {team},
title = {Generating and Certifying Accuracy Properties of Floating-Point Programs},
author = {Bonnot, Paul and Boyer, Beno{\^i}t and Faissole, Florian and March{\'e}, Claude},
hal = {https://inria.hal.science/hal-04820735},
number = {RR-9564},
institution = {Inria},
year = 2024
}
@proceedings{jfla18,
topics = {team},
title = {Vingt-neuvi\`emes Journ\'ees Francophones des Langages Applicatifs},
booktitle = {Vingt-neuvi\`emes Journ{\'e}es Francophones des Langages Applicatifs},
address = {Banyuls-sur-mer, France},
year = 2018,
month = jan,
editor = {Boldo, Sylvie and Magaud, Nicolas},
hal = {https://hal.inria.fr/hal-01707376}
}