default search action
Guillaume Melquiond
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [j19]Guillaume Melquiond, Josué Moreau:
A Safe Low-Level Language for Computer Algebra and Its Formally Verified Compiler. Proc. ACM Program. Lang. 8(ICFP): 121-146 (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
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
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
Formally Verified Approximations of Definite Integrals. J. Autom. Reason. 62(2): 281-300 (2019) - [c19]Guillaume Melquiond
Formal Verification of a State-of-the-Art Integer Square Root. ARITH 2019: 183-186 - 2018
- [b4]Jean-Michel Muller
Handbook of Floating-Point Arithmetic (2nd Ed.). Springer 2018, ISBN 978-3-319-76525-9 - [c18]Guillaume Melquiond
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
A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT. CAV (2) 2017: 419-435 - [c16]Raphaël Rieu-Helft, Claude Marché
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
Formally Verified Approximations of Definite Integrals. ITP 2016: 274-289 - 2015
- [j11]Sylvie Boldo, Jacques-Henri Jourdan
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
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
Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program. J. Autom. Reason. 50(4): 423-456 (2013) - [j7]Guillaume Melquiond
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
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
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
Handbook of Floating-Point Arithmetic. Birkhäuser 2010, ISBN 978-0-8176-4704-9, pp. I-XXIII, 1-572 - [j4]Marc Daumas
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
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
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
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-11-22 20:39 CET 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: