Guillaume Melquiond

This page is deprecated. The new one can be found at this address.

Formerly a PhD student under the supervision of Marc Daumas, in the Arénaire team of the LIP. One important contribution of this thesis is the Gappa tool. It is designed to compute bounds of arithmetic expressions in general and rounding errors of a numerical code in particular. As such, it is a tool for program certification. For increased reliability, it is also able to generate a formal proof of these bounds.

Now a post-doctoral researcher in the Mathematical Components team of the INRIA - Microsoft Research joint center. I develop efficient numerical libraries (both floating-point arithmetic and interval arithmetic) for the Coq proof assistant, as well as tactics for automatically proving inequalities on real-values expressions. These tactics are available in this library.

Publications (bibtex)

PhD thesis:

• Arithmétique d'intervalles et certification de programmes.
  Thesis (in French) and defense.

Journals:

• Emulation of FMA and correctly-rounded sums: proved algorithm using rounding to odd, with Sylvie Boldo,
  in Transactions on Computers (2008, volume 57.4). Paper.
• Formally certified floating-point filters for homogeneous geometric predicate, with Sylvain Pion,
  in Theoretical Informatics and Applications (2007, volume 41.1). Paper.
• The design of the Boost interval arithmetic library, with Hervé Brönnimann and Sylvain Pion,
  in Theoretical Computer Science (2006, volume 351). Paper.

Conferences:

• Proving bounds on real-valued functions with computations,
  for the 4th IJCAR symposium (2008, Sidney, Australia). Paper and talk.
• Floating-point arithmetic in the Coq system,
  for the 8th RNC symposium (2008, Santiago de Compostela, Spain). Paper and talk.
• Proposing Interval Arithmetic for the C++ Standard, with Hervé Brönnimann and Sylvain Pion,
  for the 12th SCAN symposium (2006, Duisburg, Germany). Talk.
• Proof and certification for an accurate discriminant, with Sylvie Boldo and Marc Daumas and William Kahan,
  for the 12th SCAN symposium (2006, Duisburg, Germany). Talk.
• Assisted verification of elementary functions using Gappa, with Florent de Dinechin and Christoph Lauter,
  for the SAC'06 symposium (2006, Dijon, France). Paper and extended paper.
• When double rounding is odd, with Sylvie Boldo,
  for the 17th IMACS symposium (2005, Paris, France). Paper and talk.
• Formal certification of arithmetic filters for geometric predicates, with Sylvain Pion,
  for the 17th IMACS symposium (2005, Paris, France). Paper and talk.
• Guaranteed proofs using interval arithmetic, with Marc Daumas and César Muñoz,
  for the 17th Arith symposium (2005, Cape Cod, USA). Paper and talk.
• Generating formally certified bounds on values and round-off errors, with Marc Daumas,
  for the 6th RNC symposium (2004, Schloß Dagstuhl, Germany). Paper and talk.
• The Boost interval library, with Hervé Brönnimann and Sylvain Pion,
  for the 5th RNC symposium (2003, Lyon, France). Paper and talk.

Various reports:

• A Proposal to add Interval Arithmetic to the C++ Standard Library, with Hervé Brönnimann and Sylvain Pion,
  for the C++ standardization committee (2006). Technical report.
• Bool_set: multi-valued logic, with Hervé Brönnimann and Sylvain Pion,
  for the C++ standardization committee (2006). Technical report.

Software:

• Library of Coq tactics for proving inequalities on real-valued expressions.
• Gappa formal tool for certifying numerical applications.
• Maintainer of the interval arithmetic library of Boost.

Contact information

Last update: November 19th, 2008.