Publications : Micaela Mayero
Back| [14] | Marie Kerjean, Micaela Mayero, and Pierre Rousselin. Maths with Coq in L1, a pedagogical experiment. In ThEdu 2024 - 13th International Workshop on Theorem proving components for Educational software, 2024. [ bib | full text on HAL ] |
| [13] | Sylvie Boldo, François Clément, David Hamelin, Micaela Mayero, and Pierre Rousselin. Teaching divisibility and binomials with Coq. In 13th International Workshop on Theorem proving components for Educational software, Nancy, France, 2024. [ bib | full text on HAL ] |
| [12] | Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, and Houda Mouhcine. Lebesgue induction and Tonelli's theorem in Coq. Research Report 9457, Inria, 2023. [ bib | full text on HAL ] |
| [11] | Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, and Houda Mouhcine. A Coq formalization of Lebesgue induction principle and Tonelli's theorem. In 25th International Symposium on Formal Methods (FM 2023), volume 14000 of Lecture Notes in Computer Science, pages 39--55, 2023. [ bib | DOI | full text on HAL ] |
| [10] | 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 ] |
| [9] |
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 |
| [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, Montpellier, France, June 2017. [ bib | full text on HAL | .pdf ] |
| [7] | 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 ] |
| [6] |
Érik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, and Laurent Théry.
Formally verified certificate checkers for hardest-to-round
computation.
Journal of Automated Reasoning, 54(1):1--29, 2015.
[ bib |
DOI |
full text on HAL ]
Keywords: formal proofs ; certificate checkers ; Hensel's lemma ; modular arithmetic |
| [5] |
Érik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, and Laurent Théry.
Formally verified certificate checkers for hardest-to-round
computation.
Journal of Automated Reasoning, pages 1--29, 2014.
[ bib |
DOI |
full text on HAL ]
Keywords: Formal proofs; Certificate checkers; Hensel’s lemma; Modular arithmetic |
| [4] | Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program. Computers and Mathematics with Applications, 68(3):325--352, 2014. [ bib | DOI | full text on HAL | http ] |
| [3] | Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Wave equation numerical resolution: a comprehensive mechanized proof of a C program. Journal of Automated Reasoning, 50(4):423--456, April 2013. [ bib | DOI | full text on HAL ] |
| [2] |
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela
Mayero, Guillaume Melquiond, and Pierre Weis.
Wave equation numerical resolution: Mathematics and program.
Research Report 7826, INRIA, December 2011.
[ bib |
full text on HAL ]
We formally prove the C program that implements a simple numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and the floating-point computation leads to round-off errors. We formally specify in Coq the numerical scheme, prove both the method error and the round-off error of the program, and derive an upper bound for the total error. This proves the adequacy of the C program to the numerical scheme and the convergence of the effective computation. To our knowledge, this is the first time a numerical analysis program is fully machine-checked. Keywords: Formal proof of numerical program; Convergence of numerical scheme; Proof of C program; Coq formal proof; Acoustic wave equation; Partial differential equation; Rounding error analysis |
| [1] | Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Formal proof of a wave equation resolution scheme: the method error. In Interactive Theorem Proving, volume 6172 of Lecture Notes in Computer Science, pages 147--162. Springer, 2010. [ bib | DOI | full text on HAL ] |
Back
This page was generated by bibtex2html.