Micaela Mayero

      

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: Fri Oct 4 17:15:49 CEST 2013

Publications


Revues internationales avec comité de lecture


[1] É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 ]
[2] 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 ]
[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. J. Autom. Reasoning, 50(4):423-456, 2013. [ bib | .pdf ]
[4] 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 ]
[5] 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, 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 ]
[2] É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 ]
[3] 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 ]
[4] 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 ]
[5] 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 ]
[6] Christine Choppy, Micaela Mayero, and Laure Petrucci. Coloured Petri net refinement specification and correctness proof with Coq. In Proceedings of NFM09, 2009. [ bib | .pdf ]
[7] 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 ]
[8] 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 ]
[9] 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 ]
[10] 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 ]
[11] 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] Micaela Mayero. Problèmes critiques et preuves formelles. Habilitation à diriger des recherches, Université Paris 13, novembre 2012. [ bib | .pdf | slides]
[2] 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 ]
[3] Micaela Mayero. The Three Gap Theorem: Specification and Proof in Coq. Technical Report 3848, INRIA, December 1999. [ bib | .html ]
[4] 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 ]
[5] 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 ]
[6] The Coq Development Team. The Coq Proof Assistant Reference Manual Version 7.2. INRIA-Rocquencourt, December 2001. [ bib | .html ]
[7] 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.97.