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 Bibtex entries
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},
doi = {10.1109/ARITH.2005.25}
}
@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},
doi = {10.1016/j.tcs.2005.09.062}
}
@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{BDKM06,
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},
doi = {10.1051/ita:2007005}
}
@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},
doi = {10.1109/TC.2007.70819}
}
@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 = {Lecture Notes in Artificial Intelligence},
doi = {10.1007/978-3-540-71070-7_2}
}
@article{RZBM09,
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},
doi = {10.1007/s10543-009-0218-z}
}
@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},
doi = {10.1109/ARITH.2009.36}
}
@inproceedings{BolFilMel09,
author = {Sylvie Boldo and Jean-Christophe Filli{\^a}tre and Guillaume Melquiond},
title = {Combining {C}oq and {G}appa 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 = {Lecture Notes in Artificial Intelligence},
doi = {10.1007/978-3-642-02614-0_10}
}
@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},
doi = {10.1145/1644001.1644003}
}
@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},
pages = {572},
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},
year = {2010},
series = {Lecture Notes on Computer Science},
address = {Edinburgh, Scotland},
editor = {Matt Kaufmann and Lawrence C. Paulson},
volume = {6172},
pages = {147--162},
doi = {10.1007/978-3-642-14052-5_12}
}
@article{DinLauMel11,
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},
volume = {60},
number = {2},
year = {2011},
publisher = {IEEE Computer Society},
pages = {242--253},
doi = {10.1109/TC.2010.128}
}
@inproceedings{BolMel11,
author = {Sylvie Boldo and Guillaume Melquiond},
title = {Flocq: A Unified Library for Proving Floating-point Algorithms in {C}oq},
booktitle = {Proceedings of the 20th IEEE Symposium on Computer Arithmetic},
editor = {Elisardo Antelo and David Hough and Paolo Ienne},
address = {T{\"u}bingen, Germany},
year = {2011},
pages = {243--252},
doi = {10.1109/ARITH.2011.40}
}
@inproceedings{LelMel12,
author = {Catherine Lelay and Guillaume Melquiond},
title = {Diff\'erentiabilit\'e et int\'egrabilit\'e en {C}oq. {A}pplication \`a la formule de d'{A}lembert},
booktitle = {23\`emes Journ\'ees Francophones des Langages Applicatifs},
year = {2012},
pages = {119--133},
address = {Carnac, France},
url = {http://hal.inria.fr/hal-00642206/fr/}
}
@inproceedings{BCCIMMM12,
author = {Fran{\c c}ois Bobot and Sylvain Conchon and {\'E}velyne Contejean and Mohamed Iguernelala and Assia Mahboubi and Alain Mebsout and Guillaume Melquiond},
title = {A {S}implex-Based Extension of {F}ourier-{M}otzkin for Solving Linear Integer Arithmetic},
booktitle = {Proceedings of the 6th International Joint Conference on Automated Reasoning},
editor = {Bernhard Gramlich and Dale Miller and Uli Sattler},
address = {Manchester, UK},
year = {2012},
pages = {67--81},
series = {Lecture Notes in Computer Science},
volume = {7364},
doi = {10.1007/978-3-642-31365-3_8}
}
@article{Mel12,
author = {Guillaume Melquiond},
title = {Floating-point arithmetic in the {C}oq system},
journal = {Information and Computation},
volume = {216},
pages = {14--23},
year = {2012},
doi = {10.1016/j.ic.2011.09.005}
}
@inproceedings{CMRI12,
author = {Sylvain Conchon and Guillaume Melquiond and Cody Roux and Mohamed Iguernelala},
title = {Built-in Treatment of an Axiomatic Floating-Point Theory for {SMT} Solvers},
booktitle = {Proceedings of the 10th International Workshop on Satisfiability Modulo Theories},
pages = {12--21},
year = {2012},
address = {Manchester, UK}
}
@inproceedings{BolLelMel12,
author = {Sylvie Boldo and Catherine Lelay and Guillaume Melquiond},
title = {Improving Real Analysis in {C}oq: a User-Friendly Approach to Integrals and Derivatives},
booktitle = {Proceedings of the 2nd International Conference on Certified Programs and Proofs},
editor = {Chris Hawblitzel and Dale Miller},
pages = {289--304},
address = {Kyoto, Japan},
year = {2012},
series = {Lecture Notes in Computer Science},
volume = {7679},
doi = {10.1007/978-3-642-35308-6_22}
}
@article{MelNowZim13,
author = {Guillaume Melquiond and W. Georg Nowak and Paul Zimmermann},
title = {Numerical approximation of the {M}asser-{G}ramain constant to four decimal digits: $\delta = 1.819...$},
journal = {Mathematics of Computation},
volume = {82},
pages = {1235--1246},
year = {2013},
publisher = {AMS},
doi = {10.1090/S0025-5718-2012-02635-4}
}
@article{BCFMMW13,
author = {Sylvie Boldo and Fran\c{c}ois Cl\'ement and Jean-Christophe Filli\^atre and Micaela Mayero and Guillaume Melquiond and Pierre Weis},
title = {Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a {C} Program},
journal = {Journal of Automated Reasoning},
volume = {50},
number = {4},
pages = {423--456},
year = {2013},
doi = {10.1007/s10817-012-9255-4}
}
@inproceedings{BJLM13,
author = {Sylvie Boldo and Jacques-Henri Jourdan and Xavier Leroy and Guillaume Melquiond},
title = {A Formally-Verified {C} Compiler Supporting Floating-Point Arithmetic},
booktitle = {Proceedings of the 21st IEEE Symposium on Computer Arithmetic},
editor = {Alberto Nannarelli and Peter-Michael Seidel and Ping Tak Peter Tang},
pages = {107--115},
year = {2013},
address = {Austin, TX, USA},
doi = {10.1109/ARITH.2013.30}
}
@inproceedings{IshMelNak13,
author = {Daisuke Ishii and Guillaume Melquiond and Shin Nakajima},
title = {Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus},
booktitle = {Proceedings of the 10th Conference on Integrated Formal Methods},
editor = {Einar Broch Johnsen and Luigia Petre},
address = {Turku, Finland},
year = {2013},
pages = {139--153},
series = {Lecture Notes in Computer Science},
volume = {7940},
doi = {10.1007/978-3-642-38613-8_10}
}
@article{MarMelMul13,
author = {\'Erik Martin-Dorel and Guillaume Melquiond and Jean-Michel Muller},
title = {Some Issues Related to Double Rounding},
journal = {BIT Numerical Mathematics},
volume = {53},
number = {4},
pages = {897--924},
year = {2013},
doi = {10.1007/s10543-013-0436-2}
}
@incollection{BolMel13,
title = {Arithm{\'e}tique des ordinateurs et preuves formelles},
author = {Sylvie Boldo and Guillaume Melquiond},
booktitle = {Informatique {M}ath{\'e}matique~: une photographie en 2013},
editor = {Philippe Langlois},
pages = {189--220},
publisher = {Presses Universitaires de Perpignan},
year = {2013}
}
@inproceedings{BFMMP13,
title = {Preserving User Proofs across Specification Changes},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
booktitle = {Proceedings of the 5th International Conference on Verified Software: Theories, Tools, and Experiments},
editor = {Ernie Cohen and Andrey Rybalchenko},
pages = {191--201},
year = {2013},
address = {Menlo Park, CA, USA},
series = {Lecture Notes in Computer Science},
volume = {8164},
doi = {10.1007/978-3-642-54108-7_10}
}
@article{BolLelMel14,
author = {Sylvie Boldo and Catherine Lelay and Guillaume Melquiond},
title = {Formalization of Real Analysis: A Survey of Proof Assistants and Libraries},
journal = {Mathematical Structures in Computer Science},
year = {2014},
doi = {10.1017/S0960129514000437}
}
@article{BCFMMW14,
author = {Sylvie Boldo and Fran\c{c}ois Cl\'ement and Jean-Christophe Filli\^atre and Micaela Mayero and Guillaume Melquiond and Pierre Weis},
title = {Trusting Computations: A Mechanized Proof from Partial Differential Equations to Actual Program},
journal = {Computers \& Mathematics with Applications},
volume = {68},
number = {3},
pages = {325--352},
year = {2014},
doi = {10.1016/j.camwa.2014.06.004}
}
@article{BJLM15,
author = {Sylvie Boldo and Jacques-Henri Jourdan and Xavier Leroy and Guillaume Melquiond},
title = {Verified Compilation of Floating-Point Computations},
journal = {Journal of Automated Reasoning},
volume = {54},
number = {2},
pages = {135--163},
year = {2015},
doi = {10.1007/s10817-014-9317-x}
}
@article{BolLelMel15,
author = {Sylvie Boldo and Catherine Lelay and Guillaume Melquiond},
title = {Coquelicot: A User-Friendly Library of Real Analysis for {C}oq},
journal = {Mathematics in Computer Science},
volume = {9},
number = {1},
pages = {41--62},
year = {2015},
doi = {10.1007/s11786-014-0181-1}
}
@article{MarMel15,
author = {{\'E}rik Martin-Dorel and Guillaume Melquiond},
title = {Proving Tight Bounds on Univariate Expressions with Elementary Functions in {C}oq},
journal = {Journal of Automated Reasoning},
pages = {1--31},
year = {2015},
doi = {10.1007/s10817-015-9350-4}
}