A Coq Formalization of Lebesgue Induction Principle and Tonelli’s Theorem

Autor: Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine

Publikováno v: Formal Methods ISBN: 9783031274800
Proceedings of the 25th International Symposium on Formal Methods
25th International Symposium on Formal Methods (FM 2023)
25th International Symposium on Formal Methods (FM 2023), Mar 2023, Lübeck, Germany. pp.39--55, ⟨10.1007/978-3-031-27481-7_4⟩
FM 2023-25th International Symposium on Formal Methods
FM 2023-25th International Symposium on Formal Methods, Mar 2023, Lübeck, Germany

International audience Lebesgue integration is a well-known mathematical tool, used for instance in probability theory, real analysis, and numerical mathematics. Thus, its formalization in a proof assistant is to be designed to fit different goals an

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b47011b3beb3b903347a18000883b4b6
https://doi.org/10.1007/978-3-031-27481-7_4

Formal proof of polynomial-time complexity with quasi-interpretations

Autor: Hugo Férée, Micaela Mayero, Samuel Hym, Jean-Yves Moyen, David Nowak

Publikováno v: 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018
7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Jan 2018, Los Angeles, United States. ⟨10.1145/3167097⟩
CPP

We present a Coq library that allows for readily proving that a function is computable in polynomial time. It is based on quasi-interpretations that, in combination with termination ordering, provide a characterisation of the class FP of functions co

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f3fc2b38614d1289da67743e27f017cc
https://hal.archives-ouvertes.fr/hal-01712390

Coloured Petri net refinement specification and correctness proof with Coq

Autor: Christine Choppy, Laure Petrucci, Micaela Mayero

Publikováno v: Innovations in Systems and Software Engineering. 6:195-202

In this work, we address the issue of the formal proof (using the proof assistant Coq) of refinement correctness for symmetric nets, a subclass of coloured Petri nets. We provide a formalisation of the net models, and of their type refinement in Coq.

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::9ee3b39ff8a2a8eb6e7fce2a0061e851
https://doi.org/10.1007/s11334-010-0131-2

Formally verified certificate checkers for hardest-to-round computation

Autor: Laurent Théry, Micaela Mayero, Guillaume Hanrot, Erik Martin-Dorel

Publikováno v: Journal of Automated Reasoning
Journal of Automated Reasoning, 2015, 54 (1), pp.1-29. ⟨10.1007/s10817-014-9312-2⟩
Journal of Automated Reasoning, Springer Verlag, 2015, 54 (1), pp.1-29. ⟨10.1007/s10817-014-9312-2⟩

International audience; In order to derive efficient and robust floating-point implementations of a given function f, it is crucial to compute its hardest-to-round points, i.e. the floating-point numbers x such that f(x) is closest to the midpoint of

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::16f848d5fda5bcc1ef494f0138e002c4
https://inria.hal.science/hal-00919498

Certified, Efficient and Sharp Univariate Taylor Models in COQ

Autor: Erik Martin-Dorel, Laurence Rideau, Ioana Pasca, Micaela Mayero, Laurent Théry

Publikováno v: SYNASC
SYNASC 2013-15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
SYNASC 2013-15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2013, Timisoara, Romania

We present a library for univariate Taylor models that has been developed with the COQ proof assistant. Each algorithm of this library is executable and has been formally proved correct. Using this library, one can then effectively compute rigorous a

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7aadeeaea799b80f96896d294b9687a1
https://doi.org/10.1109/synasc.2013.33