Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Guillaume Melquiond's pageVersion française
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.
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:
Certification of bounds on expressions involving rounded operators,
with Marc Daumas,
in Transactions on Mathematical Software (2009, volume 37.1).
Paper.
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:
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.
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.
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.
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.
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).
Directed rounding arithmetic operations,
with Sylvain Pion,
for the C++ standardization committee (2009).
Technical report.