Bibtex entries

@inproceedings{BroMelPio03,
  author    = {Herv{\'e} Br{\"o}nnimann and Guillaume Melquiond and Sylvain Pion},
  title     = {The {B}oost interval arithmetic library},
  booktitle = {Proceedings of the 5th Conference on Real Numbers and Computers},
  pages     = {65--80},
  address   = {Lyon, France},
  year      = {2003},
  url       = {http://www.lri.fr/~melquion/doc/03-rnc5-article.ps.gz}
}

@inproceedings{DauMel04,
  author    = {Marc Daumas and Guillaume Melquiond},
  title     = {Generating formally certified bounds on values and round-off errors},
  booktitle = {Proceedings of the 6th Conference on Real Numbers and Computers},
  editor    = {Vasco Brattka and Christiane Frougny and Norbert M{\"u}ller},
  pages     = {55--70},
  address   = {Schlo{\ss} Dagstuhl, Germany},
  year      = {2004},
  url       = {http://www.lri.fr/~melquion/doc/04-rnc6-article.ps.gz}
}

@inproceedings{DauMelMun05,
  author    = {Marc Daumas and Guillaume Melquiond and C{\'e}sar Mu{\~n}oz},
  title     = {Guaranteed proofs using interval arithmetic},
  booktitle = {Proceedings of the 17th IEEE Symposium on Computer Arithmetic},
  editor    = {Paolo Montuschi and Eric Schwarz},
  pages     = {188--195},
  address   = {Cape Cod, MA, USA},
  year      = {2005},
  url       = {http://www.lri.fr/~melquion/doc/05-arith17-article.pdf}
}

@inproceedings{BolMel05,
  author    = {Sylvie Boldo and Guillaume Melquiond},
  title     = {When double rounding is odd},
  booktitle = {Proceedings of the 17th IMACS World Congress on Computational and Applied Mathematics},
  address   = {Paris, France},
  year      = {2005},
  url       = {http://www.lri.fr/~melquion/doc/05-imacs17_1-article.ps.gz}
}

@inproceedings{MelPio05,
  author    = {Guillaume Melquiond and Sylvain Pion},
  title     = {Formal certification of arithmetic filters for geometric predicates},
  booktitle = {Proceedings of the 17th IMACS World Congress on Computational and Applied Mathematics},
  address   = {Paris, France},
  year      = {2005},
  url       = {http://www.lri.fr/~melquion/doc/05-imacs17_2-article.ps.gz}
}

@article{BroMelPio06a,
  author    = {Herv{\'e} Br{\"o}nnimann and Guillaume Melquiond and Sylvain Pion},
  title     = {The design of the {B}oost interval arithmetic library},
  journal   = {Theoretical Computer Science},
  editor    = {Marc Daumas and Nathalie Revol},
  pages     = {111--118},
  volume    = {351},
  year      = {2006},
  url       = {http://www.lri.fr/~melquion/doc/06-tcs-rnc5.pdf}
}

@inproceedings{DinLauMel06,
  author    = {Florent de Dinechin and Christoph Lauter and Guillaume Melquiond},
  title     = {Assisted verification of elementary functions using {G}appa},
  booktitle = {Proceedings of the 2006 ACM Symposium on Applied Computing},
  pages     = {1318--1322},
  address   = {Dijon, France},
  year      = {2006},
  url       = {http://www.lri.fr/~melquion/doc/06-mcms-article.pdf}
}

@techreport{BroMelPio06b,
  author    = {Herv{\'e} Br{\"o}nnimann and Guillaume Melquiond and Sylvain Pion},
  title     = {Bool\_set: multi-valued logic},
  institution = {ISO C++ Standardization Committee},
  number    = {2136},
  year      = {2006},
  url       = {http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n2136.pdf}
}

@techreport{BroMelPio06c,
  author    = {Herv{\'e} Br{\"o}nnimann and Guillaume Melquiond and Sylvain Pion},
  title     = {A Proposal to add Interval Arithmetic to the {C}++ Standard Library},
  institution = {ISO C++ Standardization Committee},
  number    = {2137},
  year      = {2006},
  url       = {http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n2137.pdf}
}

@inproceedings{BroMelPio06d,
  author    = {Herv{\'e} Br{\"o}nnimann and Guillaume Melquiond and Sylvain Pion},
  title     = {Proposing Interval Arithmetic for the {C}++ Standard},
  booktitle = {Proceedings of the 12th GAMM - IMACS International Symposium on
               Scientific Computing, Computer Arithmetic and Validated Numerics},
  address   = {Duisburg, Germany},
  year      = {2006}
}

@inproceedings{BolDauKahMel06,
  author    = {Sylvie Boldo and Marc Daumas and William Kahan and Guillaume Melquiond},
  title     = {Proof and certification for an accurate discriminant},
  booktitle = {Proceedings of the 12th GAMM - IMACS International Symposium on
               Scientific Computing, Computer Arithmetic and Validated Numerics},
  address   = {Duisburg, Germany},
  year      = {2006}
}

@phdthesis{Mel06,
  author    = {Guillaume Melquiond},
  title     = {De l'arithm{\'e}tique d'intervalles {\`a} la certification de programmes},
  school    = {{\'E}cole {N}ormale {S}up{\'e}rieure de {L}yon},
  address   = {Lyon, France},
  year      = {2006},
  url       = {http://www.lri.fr/~melquion/doc/06-these.pdf}
}

@article{MelPio07,
  author    = {Guillaume Melquiond and Sylvain Pion},
  title     = {Formally certified floating-point filters for homogeneous geometric predicates},
  journal   = {Theoretical Informatics and Applications},
  editor    = {Vasco Brattka and Christiane Frougny and Norbert Mueller},
  year      = {2007},
  volume    = {41},
  number    = {1},
  pages     = {57--70},
  url       = {http://www.lri.fr/~melquion/doc/07-tia.pdf}
}

@article{BolMel08,
  author    = {Sylvie Boldo and Guillaume Melquiond},
  title     = {Emulation of a {FMA} and correctly-rounded sums: Proved algorithms using rounding to odd},
  journal   = {Transactions on Computers},
  publisher = {IEEE},
  year      = {2008},
  volume    = {57},
  number    = {4},
  pages     = {462--471},
  url       = {http://www.lri.fr/~melquion/doc/08-tc.pdf}
}

@inproceedings{Mel08a,
  author    = {Guillaume Melquiond},
  title     = {Floating-point arithmetic in the {C}oq system},
  booktitle = {Proceedings of the 8th Conference on Real Numbers and Computers},
  address   = {Santiago de Compostela, Spain},
  year      = {2008},
  pages     = {93--102},
  url       = {http://www.lri.fr/~melquion/doc/08-rnc8-article.pdf}
}

@inproceedings{Mel08b,
  author    = {Guillaume Melquiond},
  title     = {Proving bounds on real-valued functions with computations},
  booktitle = {Proceedings of the 4th International Joint Conference on Automated Reasoning},
  editor    = {Alessandro Armando and Peter Baumgartner and Gilles Dowek},
  address   = {Sydney, Australia},
  year      = {2008},
  volume    = {5195},
  pages     = {2--17},
  series    = {Lectures Notes in Artificial Intelligence},
  url       = {http://www.lri.fr/~melquion/doc/08-ijcar-article.pdf}
}

@article{RumZimBolMel09,
  author    = {Siegfried M. Rump and Paul Zimmermann and Sylvie Boldo and Guillaume Melquiond},
  title     = {Computing predecessor and successor in rounding to nearest},
  journal   = {BIT Numerical Mathematics},
  year      = {2009},
  volume    = {49},
  number    = {2},
  pages     = {419--431},
  url       = {http://www.lri.fr/~melquion/doc/09-bitn.pdf}
}

@inproceedings{EdmMel09,
  author    = {William Edmonson and Guillaume Melquiond},
  title     = {{IEEE} interval standard working group - {P1788}: current status},
  booktitle = {Proceedings of the 19th IEEE Symposium on Computer Arithmetic},
  editor    = {Javier D. Bruguera and Marius Cornea and Debjit DasSarma and John Harrison},
  address   = {Portland, OR, USA},
  year      = {2009},
  pages     = {231--234},
  url       = {http://www.lri.fr/~melquion/doc/09-arith19-article.pdf}
}

@inproceedings{BolFilMel09,
  author    = {Sylvie Boldo and Jean-Christophe Filli{\^a}tre and Guillaume Melquiond},
  title     = {Combining {Coq} and {Gappa} for certifying floating-point programs},
  booktitle = {Proceedings of the 16th Calculemus Symposium},
  editor    = {Jacques Carette and Lucas Dixon and Claudio Sarcedoti Coen and Stephen M. Watt},
  address   = {Grand Bend, ON, Canada},
  year      = {2009},
  volume    = {5625},
  pages     = {59--74},
  series    = {Lectures Notes in Artificial Intelligence},
  url       = {http://www.lri.fr/~melquion/doc/09-calculemus-article.pdf}
}

@techreport{MelPio09,
  author    = {Guillaume Melquiond and Sylvain Pion},
  title     = {Directed rounding arithmetic operations},
  institution = {ISO C++ Standardization Committee},
  number    = {2899},
  year      = {2009},
  url       = {http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2009/n2899.pdf}
}

@article{DauMel10,
  author    = {Marc Daumas and Guillaume Melquiond},
  title     = {Certification of bounds on expressions involving rounded operators},
  journal   = {Transactions on Mathematical Software},
  publisher = {ACM},
  year      = {2010},
  volume    = {37},
  number    = {1},
  pages     = {1--20},
  url       = {http://www.lri.fr/~melquion/doc/09-toms.pdf}
}

@book{Mul10,
  author    = {Jean-Michel Muller and Nicolas Brisebarre and Florent de Dinechin and Claude-Pierre Jeannerod and Vincent Lef{\`e}vre and Guillaume Melquiond and Nathalie Revol and Damien Stehl{\'e} and Serge Torres},
  title     = {Handbook of Floating-Point Arithmetic},
  publisher = {Birkh{\"a}user},
  year      = {2010}
}

@inproceedings{BCFMMW10,
  author    = {Sylvie Boldo and François Cl{\'e}ment and Jean-Christophe Filli{\^a}tre and Micaela Mayero and Guillaume Melquiond and Pierre Weis},
  title     = {Formal Proof of a Wave Equation Resolution Scheme: the Method Error},
  booktitle = {Proceedings of the 1st Interactive Theorem Proving Conference (ITP)},
  year      = {2010},
  series    = {Lecture Notes on Computer Science},
  address   = {Edinburgh, Scotland},
  publisher = {Springer},
  editor    = {Matt Kaufmann and Lawrence C. Paulson},
  volume    = {6172},
  pages     = {147--162},
  url       = {http://www.lri.fr/~melquion/doc/10-itp.pdf}
}

@article{DinLauMel10,
  author    = {Florent de Dinechin and Christoph Lauter and Guillaume Melquiond},
  title     = {Certifying the Floating-point Implementation of an Elementary Function Using {Gappa}},
  journal   = {Transactions on Computers},
  year      = {2010},
  publisher = {IEEE Computer Society},
  url       = {http://www.lri.fr/~melquion/doc/10-tc.pdf}
}