עקוב אחר
Guillaume Melquiond
Guillaume Melquiond
Inria, University Paris Saclay
כתובת אימייל מאומתת בדומיין inria.fr - דף הבית
כותרת
צוטט על ידי
צוטט על ידי
שנה
Handbook of floating-point arithmetic‏
JM Muller, N Brisebarre, F De Dinechin, CP Jeannerod, L Vincent, ...‏
Birkhauser, 2009‏
1040*2009
IEEE Standard for Floating-Point Arithmetic‏
D Zuras, M Cowlishaw, A Aiken, M Applegate, D Bailey, S Bass, ...‏
IEEE Std 754-2008, 1-70, 2008‏
3262008
Flocq: A unified library for proving floating-point algorithms in Coq‏
S Boldo, G Melquiond‏
20th IEEE Symposium on Computer Arithmetic, 243-252, 2010‏
2002010
Certification of bounds on expressions involving rounded operators‏
M Daumas, G Melquiond‏
Transactions on Mathematical Software 37 (1), 1-20, 2010‏
1612010
Coquelicot: A user-friendly library of real analysis for Coq‏
S Boldo, C Lelay, G Melquiond‏
Mathematics in Computer Science 9, 41-62, 2015‏
1562015
Certifying the floating-point implementation of an elementary function using Gappa‏
F De Dinechin, C Lauter, G Melquiond‏
Transactions on Computers 60 (2), 242-253, 2011‏
1502011
Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program‏
S Boldo, F Clément, JC Filliâtre, M Mayero, G Melquiond, P Weis‏
Journal of Automated Reasoning, 2013‏
1152013
Assisted verification of elementary functions using Gappa‏
F De Dinechin, CQ Lauter, G Melquiond‏
Proceedings of the 2006 ACM symposium on Applied computing, 1318-1322, 2006‏
1152006
Combining Coq and Gappa for certifying floating-point programs‏
S Boldo, JC Filliâtre, G Melquiond‏
International Conference on Intelligent Computer Mathematics, 59-74, 2009‏
1012009
The design of the Boost interval arithmetic library‏
H Brönnimann, G Melquiond, S Pion‏
Theoretical Computer Science 351 (1), 111-118, 2006‏
932006
Formalization of real analysis: A survey of proof assistants and libraries‏
S Boldo, C Lelay, G Melquiond‏
Mathematical Structures in Computer Science 26 (7), 1196-1233, 2016‏
822016
Guaranteed proofs using interval arithmetic‏
M Daumas, G Melquiond, C Munoz‏
17th IEEE Symposium on Computer Arithmetic, 188-195, 2005‏
782005
Floating-point arithmetic in the Coq system‏
G Melquiond‏
Information and Computation 216, 14-23, 2012‏
672012
A Formally-Verified C Compiler Supporting Floating-Point Arithmetic‏
S Boldo, JH Jourdan, X Leroy, G Melquiond‏
21st IEEE Symposium on Computer Arithmetic (ARITH), 107-115, 2013‏
662013
Proving bounds on real-valued functions with computations‏
G Melquiond‏
International Joint Conference on Automated Reasoning, 2-17, 2008‏
662008
Emulation of a FMA and correctly rounded sums: Proved algorithms using rounding to odd‏
S Boldo, G Melquiond‏
IEEE Transactions on Computers 57 (4), 462-471, 2008‏
662008
Verified compilation of floating-point computations‏
S Boldo, JH Jourdan, X Leroy, G Melquiond‏
Journal of Automated Reasoning 54, 135-163, 2015‏
622015
Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System‏
S Boldo, G Melquiond‏
Elsevier, 2017‏
582017
Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program‏
S Boldo, F Clément, JC Filliâtre, M Mayero, G Melquiond, P Weis‏
532012
Formal proof of a wave equation resolution scheme: the method error‏
S Boldo, F Clément, JC Filliâtre, M Mayero, G Melquiond, P Weis‏
International Conference on Interactive Theorem Proving, 147-162, 2010‏
532010
המערכת אינה יכולה לבצע את הפעולה כעת. נסה שוב מאוחר יותר.
מאמרים 1–20