@inproceedings{FM23,
author = {Sylvie Boldo and Fran{\c{c}}ois Cl{\'{e}}ment and
Vincent Martin and Micaela Mayero and Houda Mouhcine},
title = {Lebesgue Induction and Tonelli's Theorem in Coq},
booktitle = {Formal Methods - 25th International Symposium, {FM}, Proceedings},
series = {LNCS},
volume = {14000},
pages = {39--55},
publisher = {Springer},
year = {2023},
url = {https://hal.archives-ouvertes.fr/hal-03564379/}
}
@inproceedings{CPP2018,
author = {Hugo F{\'{e}}r{\'{e}}e and
Samuel Hym and
Micaela Mayero and
Jean{-}Yves Moyen and
David Nowak},
title = {Formal proof of polynomial-time complexity with quasi-interpretations},
booktitle = {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},
year = {2018},
http = {http://www-lipn.univ-paris13.fr/~mayero/publis/CPP2018.pdf}
}
@inproceedings{CPP2017,
author = {Sylvie Boldo and
Fran{\c{c}}ois Cl{\'{e}}ment and
Florian Faissole and
Vincent Martin and
Micaela Mayero},
title = {A Coq formal proof of the LaxMilgram theorem},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {79--89},
year = {2017},
http = {https://hal.inria.fr/hal-01391578}
}
@inproceedings{SYNASC2013,
author = {{\'{E}}rik Martin{-}Dorel and
Laurence Rideau and
Laurent Th{\'{e}}ry and
Micaela Mayero and
Ioana Pasca},
title = {Certified, Efficient and Sharp Univariate Taylor Models in {COQ}},
booktitle = {15th International Symposium on Symbolic and Numeric Algorithms for
Scientific Computing, {SYNASC} 2013, Timisoara, Romania, September
23-26, 2013},
pages = {193--200},
year = {2013},
http = {http://hal.inria.fr/docs/00/86/92/47/PDF/CoqApprox2013_HAL_v2.pdf}
}
@inproceedings{NFM2012,
author = {Brisebarre, Nicolas and Joldes, Mioara and Martin-Dorel, Erik and Mayero, Micaela and Muller, Jean-Michel and Pasca, Ioana and Rideau, Laurence and Théry, Laurent},
title = {{R}igorous {P}olynomial {A}pproximations using {T}aylor {M}odels in {C}oq},
booktitle = {Proceedings of NFM 2012 (Nasa Formal Methods)},
publisher = {Springer-Verlag LNCS},
volume = {7226},
pages = {85-99},
year = {2012},
http = {http://www-lipn.univ-paris13.fr/~mayero/publis/RPA-NFM.pdf}
}
@inproceedings{Calculemus2010,
author = {Butelle, Franck and Hivert, Florent and Mayero, Micaela and Toumazet, Frédéric},
title = {{F}ormal {P}roof of {SCHUR} {C}onjugate {F}unction},
booktitle = {Proceedings of Calculemus 2010},
publisher = {Springer-Verlag LNAI},
pages = {158-171},
year = {2010},
http = {http://www-lipn.univ-paris13.fr/~mayero/publis/Calculemus2010.pdf}
}
@inproceedings{ITP2010,
author = {Boldo, Sylvie and Clément, François and Filliâtre, Jean-Christophe and
Mayero, Micaela and Melquiond, Guillaume and Weis, Pierre},
title = {{F}ormal {P}roof of a {W}ave {E}quation {R}esolution {S}cheme: the {M}ethod
{E}rror},
booktitle = {Proceedings of ITP 2010 (Interactive Theorem Proving)},
publisher = {Springer-Verlag LNCS},
pages = {147-162},
year = {2010},
http = {http://www-lipn.univ-paris13.fr/~mayero/publis/ITP2010.pdf}
}
@inproceedings{CC-MM-LP-NFM09,
author = {Choppy, Christine and Mayero, Micaela and
Petrucci, Laure},
title = {{C}oloured {P}etri net refinement specification
and correctness proof with {C}oq},
booktitle = {Proceedings of NFM09},
year = {2009},
http = {http://www-lipn.univ-paris13.fr/~mayero/publis/nfm09.pdf}
}
@inproceedings{BM-FV-MM-NV-CISST09,
author = {Bruno Monsuez and
Franck Védrine and
Micaela Mayero and
Nicolas Vallée},
title = {How an "Incoherent Behavior" inside generic hardware component characterizes functional errors ?},
booktitle = {Proceedings of AIKED'09 Artificial Intelligence, Knowledge
Engineering & Data bases)},
year = {2009},
http = {http://www-lipn.univ-paris13.fr/~mayero/publis/cisst09.pdf}
}
@inproceedings{CC-MM-LP-Refine2008,
author = {Christine Choppy and
Micaela Mayero and
Laure Petrucci},
title = {Experimenting Formal Proofs of Petri Nets Refinements},
booktitle = {Proceedings of REFINE 2008, Electr. Notes Theor. Comput. Sci.},
volume = {214},
year = {2008},
pages = {231-254},
ee = {http://dx.doi.org/10.1016/j.entcs.2008.06.011},
bibsource = {DBLP, http://dblp.uni-trier.de},
http = {http://www-lipn.univ-paris13.fr/~mayero/publis/Refine08.pdf}
}
@inproceedings{MM-DD-Calculemus2005,
author = {Delahaye, David and Mayero, Micaela},
title = {{Q}uantifier {E}limination over {A}lgebraically
{C}losed {F}ields in a
{P}roof {A}ssistant using a {C}omputer
{A}lgebra {S}ystem},
booktitle = {Proceedings of Calculemus 2005},
volume = {151(1)},
pages = {57--73},
series = {ENTCS},
year = {2006},
http = {http://www-lipn.univ-paris13.fr/~mayero/publis/Calculemus05_qelim.pdf}
}
@inproceedings{MM-tphol2002,
author = {Mayero, Micaela},
title = {{U}sing {T}heorem {P}roving for {N}umerical
{A}nalysis.
{C}orrectness {P}roof of al {A}utomatic
{D}ifferentiation {A}lgorithm},
booktitle = {Proceedings of TPHOLs2002 (Theorem Proving in Higher Order Logics)},
publisher = {Springer-Verlag LNCS},
volume = {2410},
pages = {246},
year = {2002},
http = {http://www-lipn.univ-paris13.fr/~mayero/publis/odyssee.ps.gz}
}
@inproceedings{three-gap-types99,
author = {Mayero, Micaela},
title = {{T}he {T}hree {G}ap {T}heorem
(Steinhauss Conjecture)},
booktitle = {Proceedings of TYPES'99},
publisher = {Springer-Verlag LNCS},
volume = {1956},
pages = {162--173},
year = {2000},
http = {http://www-lipn.univ-paris13.fr/~mayero/publis/three-gap.ps.gz}
}
This file was generated by bibtex2html 1.99.