Guillaume Melquiond

I am an INRIA researcher in the Proval team from the LRI (Université Paris Sud).

My research interests are floating-point and interval arithmetic, and formal proof. I am working on methods for formally certifying the correctness (behavior and accuracy) of numerical applications; these methods are implemented in the Gappa tool. I am also working on using numerical computations for formally proving mathematical theorems; there is now a library of tactics for the Coq proof assistant. Finally, I'm developing Flocq, a generic formalization of floating-point arithmetic in Coq.

Publications (bibtex)

Book and PhD thesis:

• Handbook of Floating-Point Arithmetic, coordinated by Jean-Michel Muller,
  published by Birkhäuser. Summary.
• Arithmétique d'intervalles et certification de programmes.
  Thesis (in French) and defense.

Journals:

• Certifying the floating-point implementation of an elementary function using Gappa, with Florent de Dinechin and Christoph Lauter,
  in Transactions on Computers (2011, volume 60.2). Paper. DOI.
• Certification of bounds on expressions involving rounded operators, with Marc Daumas,
  in Transactions on Mathematical Software (2010, volume 37.1). Paper. DOI.
• Computing predecessor and successor in rounding to nearest, with Sylvie Boldo, Siegfried Rump, and Paul Zimmermann,
  in BIT Numerical Mathematics (2009, volume 49.2). Paper. DOI.
• 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. DOI.
• Formally certified floating-point filters for homogeneous geometric predicate, with Sylvain Pion,
  in Theoretical Informatics and Applications (2007, volume 41.1). Paper. DOI.
• The design of the Boost interval arithmetic library, with Hervé Brönnimann and Sylvain Pion,
  in Theoretical Computer Science (2006, volume 351). Paper. DOI.

Conferences:

• Différentiabilité et intégrabilité en Coq. Application à la formule de d'Alembert, with Catherine Lelay,
  for the 23th JFLA meeting (2012, Carnac, France). Paper.
• Flocq: a unified library for proving floating-point algorithms in Coq, with Sylvie Boldo,
  for the 20th ARITH symposium (2011, Tübingen, Germany). Paper and talk. DOI.
• Formal proof of a wave equation resolution scheme: the method error, with Sylvie Boldo, François Clément, Micaela Mayero, Jean-Christophe Filliâtre, and Pierre Weis,
  for the 1st ITP symposium (2010, Edinburgh, Scotland). Paper. DOI.
• Combining Coq and Gappa for certifying floating-point programs, with Sylvie Boldo and Jean-Christophe Filliâtre,
  for the 16th Calculemus symposium (2009, Grand Bend, ON, Canada). Paper and talk. DOI.
• Proving bounds on real-valued functions with computations,
  for the 4th IJCAR symposium (2008, Sidney, Australia). Paper and talk. DOI.
• 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, 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, MA, USA). Paper and talk. DOI.
• 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.

Some reports:

• IEEE interval standard working group - P1788: current status, with William Edmonson,
  for the 19th Arith symposium (2009, Portland, OR, USA). Paper and talk (first part). DOI.
• Directed rounding arithmetic operations, with Sylvain Pion,
  for the C++ standardization committee (2009). Technical report.
• 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 contributions

• Library of Coq tactics for proving inequalities on real-valued expressions.
• Flocq: a multi-radix multi-format multi-precision formalization of floating-point arithmetic in Coq.
• Gappa: a tool for formally certifying numerical applications.
• Contributor to Why and Frama-C.
• Maintainer of the interval arithmetic library of Boost.

Contact information

Last update: March 30th, 2012.