| [1] | Micaela Mayero.
The Three Gap Theorem (steinhauss conjecture).
In Proceedings of TYPES'99, volume 1956, pages 162-173.
Springer-Verlag LNCS.
ftp://ftp.inria.fr/INRIA/LogiCal/Micaela.Mayero/papers/three-gap.ps.gz. BibTeX entry
|
| [2] | Micaela Mayero.
Using Theorem Proving for Numerical Analysis. Correctness
Proof of al Automatic Differentiation Algorithm.
In Proceedings of TPHOLs2002, volume 2410, page 246.
Springer-Verlag LNCS.
ftp://ftp.inria.fr/INRIA/LogiCal/Micaela.Mayero/papers/odyssee.ps.gz. BibTeX entry
|
| [3] | 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.
ftp://ftp.inria.fr/INRIA/LogiCal/Micaela.Mayero/papers/Maple-Mode.ps.gz. BibTeX entry
|
| [4] | 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.
ftp://ftp.inria.fr/INRIA/LogiCal/Micaela.Mayero/papers/field.ps.gz. BibTeX entry
|
| [5] | Micaela Mayero.
The Three Gap Theorem: Specification and Proof in Coq.
Technical Report 3848, INRIA, December 1999.
ftp://ftp.inria.fr/INRIA/publication/publi-ps-gz/RR/RR-3848.ps.gz. BibTeX entry
|
| [6] | 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.
ftp://ftp.inria.fr/INRIA/LogiCal/Micaela.Mayero/papers/field-pvs.ps.gz. BibTeX entry
|
| [7] | Micaela Mayero.
Formalisation et automatisation de preuves en analyses réelle
et numérique.
PhD thesis, Université Paris VI, décembre 2001.
ftp://ftp.inria.fr/INRIA/LogiCal/Micaela.Mayero/papers/these-mayero.ps.gz. BibTeX entry
|
| [8] | The Coq Development Team.
The Coq Proof Assistant Reference Manual Version 7.2.
INRIA-Rocquencourt, December 2001.
http://coq.inria.fr/doc-eng.html. BibTeX entry
|
| [9] | 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.
ftp://ftp.inria.fr/INRIA/LogiCal/Micaela.Mayero/papers/DEA97-mayero.ps.gz. BibTeX entry
|