|
Contacts:
LIPN - UMR CNRS 7030
Institut Galilée - Université Paris Nord
99 avenue Jean-Baptiste Clément
93430 Villetaneuse
FRANCE
Tél.
Fax
: +33 (0) 1 49 40 36 91
: +33 (0) 1 48 26 07 12
Micaela.Mayero [at] lipn.univ-paris13.fr
Bureau
: A209
English version
Last modified: Thu Mar 21 17:15:49 CEST 2024
|
Publications
biblio-J
Revues internationales avec comité de lecture
|
[1]
|
Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela
Mayero.
A coq formalization of lebesgue integration of nonnegative functions.
J. Autom. Reasoning, 66(2):175--213, 2022.
[ bib |
http ]
|
|
[2]
|
Érik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, and Laurent
Théry.
Formally verified certificate checkers for hardest-to-round
computation.
J. Autom. Reasoning, 54(1):1--29, 2015.
[ bib |
.pdf ]
|
|
[3]
|
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 & Mathematics with Applications, 68(3):325--352,
2014.
[ bib |
http ]
|
|
[4]
|
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.
J. Autom. Reasoning, 50(4):423--456, 2013.
[ bib |
.pdf ]
|
|
[5]
|
Christine Choppy, Micaela Mayero, and Laure Petrucci.
Coloured Petri net refinement specification and correctness proof
with Coq.
volume 6, pages 195--202, 2010.
[ bib |
.pdf ]
|
|
[6]
|
David Delahaye and Micaela Mayero.
Dealing with Algebraic Expressions over a Field in Coq
using Maple.
In Journal of Symbolic Computation: special issue on the
integration of automated reasoning and computer algebra systems, volume 39,
pages 569--592, 2005.
[ bib |
.ps.gz ]
|
Conférences internationales avec comité de lecture
|
[1]
|
Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, and
Houda Mouhcine.
Lebesgue induction and tonelli's theorem in coq.
In
Formal Methods - 25th International Symposium, FM, Proceedings, LNCS,
volume 14000, pages 39--55}, 2023.
[ bib |
http ]
|
|
[2]
|
Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, and
David Nowak.
Formal proof of polynomial-time complexity with
quasi-interpretations.
In Proceedings of the 7th ACM SIGPLAN International
Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA,
USA, January 8-9, 2018, pages 146--157, 2018.
[ bib |
.pdf ]
|
|
[3]
|
Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin,
and Micaela Mayero.
A coq formal proof of the laxmilgram theorem.
In Proceedings of the 6th ACM SIGPLAN Conference on
Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17,
2017, pages 79--89, 2017.
[ bib |
http ]
|
|
[4]
|
Érik Martin-Dorel, Laurence Rideau, Laurent Théry, Micaela
Mayero, and Ioana Pasca.
Certified, efficient and sharp univariate taylor models in COQ.
In 15th International Symposium on Symbolic and Numeric
Algorithms for Scientific Computing, SYNASC 2013, Timisoara, Romania,
September 23-26, 2013, pages 193--200, 2013.
[ bib |
.pdf ]
|
|
[5]
|
Nicolas Brisebarre, Mioara Joldes, Erik Martin-Dorel, Micaela Mayero,
Jean-Michel Muller, Ioana Pasca, Laurence Rideau, and Laurent Théry.
Rigorous Polynomial Approximations using Taylor Models in
Coq.
In Proceedings of NFM 2012 (Nasa Formal Methods), volume 7226,
pages 85--99. Springer-Verlag LNCS, 2012.
[ bib |
.pdf ]
|
|
[6]
|
Franck Butelle, Florent Hivert, Micaela Mayero, and Frédéric Toumazet.
Formal Proof of SCHUR Conjugate Function.
In Proceedings of Calculemus 2010, pages 158--171.
Springer-Verlag LNAI, 2010.
[ bib |
.pdf ]
|
|
[7]
|
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 Proceedings of ITP 2010 (Interactive Theorem Proving), pages
147--162. Springer-Verlag LNCS, 2010.
[ bib |
.pdf ]
|
|
[8]
|
Christine Choppy, Micaela Mayero, and Laure Petrucci.
Coloured Petri net refinement specification and correctness proof
with Coq.
In Proceedings of NFM09, 2009.
[ bib |
.pdf ]
|
|
[9]
|
Bruno Monsuez, Franck Védrine, Micaela Mayero, and Nicolas Vallée.
How an "incoherent behavior" inside generic hardware component
characterizes functional errors ?
In Proceedings of AIKED'09 Artificial Intelligence, Knowledge
Engineering & Data bases), 2009.
[ bib |
.pdf ]
|
|
[10]
|
Christine Choppy, Micaela Mayero, and Laure Petrucci.
Experimenting formal proofs of petri nets refinements.
In Proceedings of REFINE 2008, Electr. Notes Theor. Comput.
Sci., volume 214, pages 231--254, 2008.
[ bib |
.pdf ]
|
|
[11]
|
David Delahaye and Micaela Mayero.
Quantifier Elimination over Algebraically Closed Fields in
a Proof Assistant using a Computer Algebra System.
In Proceedings of Calculemus 2005, volume 151(1) of
ENTCS, pages 57--73, 2006.
[ bib |
.pdf ]
|
|
[12]
|
Micaela Mayero.
Using Theorem Proving for Numerical Analysis. Correctness
Proof of al Automatic Differentiation Algorithm.
In Proceedings of TPHOLs2002 (Theorem Proving in Higher Order
Logics), volume 2410, page 246. Springer-Verlag LNCS, 2002.
[ bib |
.ps.gz ]
|
|
[13]
|
Micaela Mayero.
The Three Gap Theorem (steinhauss conjecture).
In Proceedings of TYPES'99, volume 1956, pages 162--173.
Springer-Verlag LNCS, 2000.
[ bib |
.ps.gz ]
|
Conférences francophones avec comité de lecture
|
[1]
|
David Delahaye and Micaela Mayero.
Field: une procédure de décision pour les nombres réels
en Coq.
In Journées Francophones des Langages Applicatifs,
Pontarlier. INRIA, Janvier 2001.
[ bib |
.ps.gz ]
|
Autres
|
[1]
|
Marie Kerjean, Frédéric Le Roux, Patrick Massot, Micaela Mayero, Zoé Mesnil,
Simon Modeste, Julien Narboux, and Pierre Rousselin.
Utilisation des assistants de preuves pour l'enseignement en L1.
In Gazette de la SMF, volume 174, Octobre 2022.
[ bib |
.pdf ]
|
|
[2]
|
Micaela Mayero.
Problèmes critiques et preuves formelles.
Habilitation à diriger des recherches, Université Paris 13,
novembre 2012.
[ bib |
.pdf ]
|
|
[3]
|
David Delahaye and Micaela Mayero.
Diophantus' 20th Problem and Fermat's Last Theorem for n=4:
Formalization of Fermat's Proofs in the Coq Proof Assistant.
Technical report, 2005.
[ bib |
http ]
|
|
[4]
|
Micaela Mayero.
The Three Gap Theorem: Specification and Proof in Coq.
Technical Report 3848, INRIA, December 1999.
[ bib |
.html ]
|
|
[5]
|
César Muñoz and Micaela Mayero.
Real Automation in the Field.
Technical Report NASA/CR-2001-211271 Report 39, ICASE Nasa-Langley
Research Center, December 2001.
[ bib |
.ps.gz ]
|
|
[6]
|
Micaela Mayero.
Formalisation et automatisation de preuves en analyses réelle
et numérique.
PhD thesis, Université Paris VI, décembre 2001.
[ bib |
.ps.gz ]
|
|
[7]
|
The Coq Development Team.
The Coq Proof Assistant Reference Manual Version 7.2.
INRIA-Rocquencourt, December 2001.
[ bib |
.html ]
|
|
[8]
|
Micaela Mayero.
Le théorème des 3 intervalles: spécification et preuve en
Coq.
Rapport du dea sémantique, preuves et programmation, Université
Pierre et Marie Curie (Paris 6), Septembre 1997.
[ bib |
.ps.gz ]
|
This file was generated by
bibtex2html 1.99.
|
