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}
}
@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}
}