default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDGuillaume Melquiond
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[c25]Florian Faissole, Paul Geneau de Lamarlière, Guillaume Melquiond:
End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation. ITP 2024: 14:1-14:18- 2023
- [j18]Sylvie Boldo, Claude-Pierre Jeannerod, Guillaume Melquiond, Jean-Michel Muller
:
Floating-point arithmetic. Acta Numer. 32: 203-290 (2023) - [j17]Érik Martin-Dorel, Guillaume Melquiond, Pierre Roux:
Enabling Floating-Point Arithmetic in the Coq Proof Assistant. J. Autom. Reason. 67(4): 33 (2023) - [j16]Guillaume Melquiond, Raphaël Rieu-Helft:
WhyMP, a formally verified arbitrary-precision integer library. J. Symb. Comput. 115: 74-95 (2023) - [j15]Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond:
A strong call-by-need calculus. Log. Methods Comput. Sci. 19(1) (2023) - [c24]Paul Geneau de Lamarlière, Guillaume Melquiond, Florian Faissole:
Slimmer Formal Proofs for Mathematical Libraries. ARITH 2023: 32-35 - 2021
- [c23]Sylvie Boldo, Guillaume Melquiond:
Some Formal Tools for Computer Arithmetic: Flocq and Gappa. ARITH 2021: 111-114 - [c22]Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond:
A Strong Call-By-Need Calculus. FSCD 2021: 9:1-9:22 - [c21]Guillaume Melquiond:
Plotting in a Formally Verified Way. F-IDE@NFM 2021: 39-45 - [i7]Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond:
A strong call-by-need calculus. CoRR abs/2111.01485 (2021) - 2020
- [c20]Guillaume Melquiond, Raphaël Rieu-Helft:
WhyMP, a formally verified arbitrary-precision integer library. ISSAC 2020: 352-359
2010 – 2019
- 2019
- [b5]Guillaume Melquiond:
Formal Verification for Numerical Computations, and the Other Way Around. University of Paris-Sud, Orsay, France, 2019 - [j14]Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote:
Formally Verified Approximations of Definite Integrals. J. Autom. Reason. 62(2): 281-300 (2019) - [c19]Guillaume Melquiond, Raphaël Rieu-Helft:
Formal Verification of a State-of-the-Art Integer Square Root. ARITH 2019: 183-186 - 2018
- [b4]Jean-Michel Muller, Nicolas Brunie, Florent de Dinechin, Claude-Pierre Jeannerod, Mioara Joldes, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, Serge Torres:
Handbook of Floating-Point Arithmetic (2nd Ed.). Springer 2018, ISBN 978-3-319-76525-9 - [c18]Guillaume Melquiond, Raphaël Rieu-Helft:
A Why3 Framework for Reflection Proofs and Its Application to GMP's Algorithms. IJCAR 2018: 178-193 - 2017
- [b3]Sylvie Boldo, Guillaume Melquiond:
Computer Arithmetic and Formal Proofs - Verifying Floating-point Algorithms with the Coq System. ISTE Press 2017, ISBN 978-1-7854-8112-3, pp. I-XX, 1-306 - [c17]Sylvain Conchon, Mohamed Iguernelala, Kailiang Ji, Guillaume Melquiond, Clément Fumex:
A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT. CAV (2) 2017: 419-435 - [c16]Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond:
How to Get an Efficient yet Verified Arbitrary-Precision Integer Library. VSTTE 2017: 84-101 - 2016
- [j13]Érik Martin-Dorel, Guillaume Melquiond:
Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq. J. Autom. Reason. 57(3): 187-217 (2016) - [j12]Sylvie Boldo, Catherine Lelay, Guillaume Melquiond:
Formalization of real analysis: a survey of proof assistants and libraries. Math. Struct. Comput. Sci. 26(7): 1196-1233 (2016) - [c15]Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote:
Formally Verified Approximations of Definite Integrals. ITP 2016: 274-289 - 2015
- [j11]Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond:
Verified Compilation of Floating-Point Computations. J. Autom. Reason. 54(2): 135-163 (2015) - [j10]Sylvie Boldo, Catherine Lelay, Guillaume Melquiond:
Coquelicot: A User-Friendly Library of Real Analysis for Coq. Math. Comput. Sci. 9(1): 41-62 (2015) - 2014
- [j9]Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis:
Trusting computations: A mechanized proof from partial differential equations to actual program. Comput. Math. Appl. 68(3): 325-352 (2014) - [c14]Guillaume Melquiond:
Automating the Verification of Floating-Point Algorithms. SMT 2014: 63 - 2013
- [j8]Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis:
Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program. J. Autom. Reason. 50(4): 423-456 (2013) - [j7]Guillaume Melquiond, W. Georg Nowak, Paul Zimmermann:
Numerical approximation of The Masser-Gramain constant to four decimal digits: δ = 1.819.... Math. Comput. 82(282): 1235-1246 (2013) - [c13]Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond:
A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. IEEE Symposium on Computer Arithmetic 2013: 107-115 - [c12]Daisuke Ishii, Guillaume Melquiond, Shin Nakajima:
Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus. IFM 2013: 139-153 - [c11]François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich:
Preserving User Proofs across Specification Changes. VSTTE 2013: 191-201 - 2012
- [j6]Guillaume Melquiond:
Floating-point arithmetic in the Coq system. Inf. Comput. 216: 14-23 (2012) - [c10]Sylvain Conchon, Guillaume Melquiond, Cody Roux, Mohamed Iguernelala:
Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers. SMT@IJCAR 2012: 12-21 - [c9]François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond:
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic. IJCAR 2012: 67-81 - [c8]Sylvie Boldo, Catherine Lelay, Guillaume Melquiond:
Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives. CPP 2012: 289-304 - [i6]Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis:
Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program. CoRR abs/1212.6641 (2012) - 2011
- [j5]Florent de Dinechin, Christoph Quirin Lauter, Guillaume Melquiond:
Certifying the Floating-Point Implementation of an Elementary Function Using Gappa. IEEE Trans. Computers 60(2): 242-253 (2011) - [c7]Sylvie Boldo, Guillaume Melquiond:
Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq. IEEE Symposium on Computer Arithmetic 2011: 243-252 - [i5]Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis:
Wave Equation Numerical Resolution: Mathematics and Program. CoRR abs/1112.1795 (2011) - 2010
- [b2]Jean-Michel Muller, Nicolas Brisebarre, Florent de Dinechin, Claude-Pierre Jeannerod, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, Damien Stehlé, Serge Torres:
Handbook of Floating-Point Arithmetic. Birkhäuser 2010, ISBN 978-0-8176-4704-9, pp. I-XXIII, 1-572 - [j4]Marc Daumas, Guillaume Melquiond:
Certification of bounds on expressions involving rounded operators. ACM Trans. Math. Softw. 37(1): 2:1-2:20 (2010) - [c6]Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis:
Formal Proof of a Wave Equation Resolution Scheme: The Method Error. ITP 2010: 147-162 - [i4]Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis:
Formal Proof of a Wave Equation Resolution Scheme: the Method Error. CoRR abs/1005.0824 (2010)
2000 – 2009
- 2009
- [c5]William W. Edmonson, Guillaume Melquiond:
IEEE Interval Standard Working Group - P1788: Current Status. IEEE Symposium on Computer Arithmetic 2009: 231-234 - [c4]Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond:
Combining Coq and Gappa for Certifying Floating-Point Programs. Calculemus/MKM 2009: 59-74 - 2008
- [j3]Sylvie Boldo, Guillaume Melquiond:
Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd. IEEE Trans. Computers 57(4): 462-471 (2008) - [c3]Guillaume Melquiond:
Proving Bounds on Real-Valued Functions with Computations. IJCAR 2008: 2-17 - [i3]Florent de Dinechin, Christoph Quirin Lauter, Guillaume Melquiond:
Certifying floating-point implementations using Gappa. CoRR abs/0801.0523 (2008) - 2007
- [j2]Guillaume Melquiond, Sylvain Pion:
Formally certified floating-point filters for homogeneous geometric predicates. RAIRO Theor. Informatics Appl. 41(1): 57-69 (2007) - [i2]Marc Daumas, Guillaume Melquiond:
Certification of bounds on expressions involving rounded operators. CoRR abs/cs/0701186 (2007) - 2006
- [b1]Guillaume Melquiond:
De l'arithmétique d'intervalles à la certification de programmes. (From interval arithmetic to program verification). École normale supérieure de Lyon, France, 2006 - [j1]Hervé Brönnimann, Guillaume Melquiond, Sylvain Pion:
The design of the Boost interval arithmetic library. Theor. Comput. Sci. 351(1): 111-118 (2006) - [c2]Florent de Dinechin, Christoph Quirin Lauter, Guillaume Melquiond:
Assisted verification of elementary functions using Gappa. SAC 2006: 1318-1322 - [i1]Sylvain Pion, Hervé Brönnimann, Guillaume Melquiond:
A Proposal to add Interval Arithmetic to the C++ Standard Library. Reliable Implementation of Real Number Algorithms 2006 - 2005
- [c1]Marc Daumas, Guillaume Melquiond, César A. Muñoz:
Guaranteed Proofs Using Interval Arithmetic. IEEE Symposium on Computer Arithmetic 2005: 188-195
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 22:12 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
