Guillaume Melquiond

ORCID

Publication Activity (10 Years)

Years Active: 2005-2023
Publications (10 Years): 18

Top Venues

École normale supérieure de Lyon, France (PHD)

Education History

École normale supérieure de Lyon, France

PHD

Publications

Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond
A strong call-by-need calculus. Log. Methods Comput. Sci. 19 (1) (2023)
Paul Geneau de Lamarlière, Guillaume Melquiond, Florian Faissole
Slimmer Formal Proofs for Mathematical Libraries. ARITH (2023)
Guillaume Melquiond, Raphaël Rieu-Helft
WhyMP, a formally verified arbitrary-precision integer library. J. Symb. Comput. 115 (2023)
Sylvie Boldo, Claude-Pierre Jeannerod, Guillaume Melquiond, Jean-Michel Muller
Floating-point arithmetic. Acta Numer. 32 (2023)
Érik Martin-Dorel, Guillaume Melquiond, Pierre Roux
Enabling Floating-Point Arithmetic in the Coq Proof Assistant. J. Autom. Reason. 67 (4) (2023)
Sylvie Boldo, Guillaume Melquiond
Some Formal Tools for Computer Arithmetic: Flocq and Gappa. ARITH (2021)
Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond
A Strong Call-By-Need Calculus. FSCD (2021)
Guillaume Melquiond
Plotting in a Formally Verified Way. F-IDE@NFM (2021)
Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond
A strong call-by-need calculus. CoRR (2021)
Guillaume Melquiond, Raphaël Rieu-Helft
WhyMP, a formally verified arbitrary-precision integer library. ISSAC (2020)
Guillaume Melquiond, Raphaël Rieu-Helft
Formal Verification of a State-of-the-Art Integer Square Root. ARITH (2019)
Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
Formally Verified Approximations of Definite Integrals. J. Autom. Reason. 62 (2) (2019)
Guillaume Melquiond, Raphaël Rieu-Helft
A Why3 Framework for Reflection Proofs and Its Application to GMP's Algorithms. IJCAR (2018)
Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond
How to Get an Efficient yet Verified Arbitrary-Precision Integer Library. VSTTE (2017)
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)
Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
Formalization of real analysis: a survey of proof assistants and libraries. Math. Struct. Comput. Sci. 26 (7) (2016)
Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
Formally Verified Approximations of Definite Integrals. ITP (2016)
Érik Martin-Dorel, Guillaume Melquiond
Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq. J. Autom. Reason. 57 (3) (2016)
Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
Coquelicot: A User-Friendly Library of Real Analysis for Coq. Math. Comput. Sci. 9 (1) (2015)
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
Verified Compilation of Floating-Point Computations. J. Autom. Reason. 54 (2) (2015)
Guillaume Melquiond
Automating the Verification of Floating-Point Algorithms. SMT (2014)
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) (2014)
Daisuke Ishii, Guillaume Melquiond, Shin Nakajima
Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus. IFM (2013)
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. IEEE Symposium on Computer Arithmetic (2013)
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich
Preserving User Proofs across Specification Changes. VSTTE (2013)
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) (2013)
Guillaume Melquiond, W. Georg Nowak, Paul Zimmermann
Numerical approximation of The Masser-Gramain constant to four decimal digits: δ = 1.819.... Math. Comput. 82 (282) (2013)
Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives. CPP (2012)
Sylvain Conchon, Guillaume Melquiond, Cody Roux, Mohamed Iguernelala
Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers. SMT@IJCAR (2012)
Guillaume Melquiond
Floating-point arithmetic in the Coq system. Inf. Comput. 216 (2012)
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 (2012)
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)
Sylvie Boldo, Guillaume Melquiond
Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq. IEEE Symposium on Computer Arithmetic (2011)
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
Wave Equation Numerical Resolution: Mathematics and Program CoRR (2011)
Florent de Dinechin, Christoph Quirin Lauter, Guillaume Melquiond
Certifying the Floating-Point Implementation of an Elementary Function Using Gappa. IEEE Trans. Computers 60 (2) (2011)
Marc Daumas, Guillaume Melquiond
Certification of bounds on expressions involving rounded operators. ACM Trans. Math. Softw. 37 (1) (2010)
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 (2010)
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)
William W. Edmonson, Guillaume Melquiond
IEEE Interval Standard Working Group - P1788: Current Status. IEEE Symposium on Computer Arithmetic (2009)
Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond
Combining Coq and Gappa for Certifying Floating-Point Programs. Calculemus/MKM (2009)
Sylvie Boldo, Guillaume Melquiond
Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd. IEEE Trans. Computers 57 (4) (2008)
Guillaume Melquiond
Proving Bounds on Real-Valued Functions with Computations. IJCAR (2008)
Florent de Dinechin, Christoph Quirin Lauter, Guillaume Melquiond
Certifying floating-point implementations using Gappa CoRR (2008)
Marc Daumas, Guillaume Melquiond
Certification of bounds on expressions involving rounded operators CoRR (2007)
Guillaume Melquiond, Sylvain Pion
Formally certified floating-point filters for homogeneous geometric predicates. RAIRO Theor. Informatics Appl. 41 (1) (2007)
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)
Hervé Brönnimann, Guillaume Melquiond, Sylvain Pion
The design of the Boost interval arithmetic library. Theor. Comput. Sci. 351 (1) (2006)
Florent de Dinechin, Christoph Quirin Lauter, Guillaume Melquiond
Assisted verification of elementary functions using Gappa. SAC (2006)
Marc Daumas, Guillaume Melquiond, César A. Muñoz
Guaranteed Proofs Using Interval Arithmetic. IEEE Symposium on Computer Arithmetic (2005)

Guillaume Melquiond.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Guillaume Melquiond