Guillaume Melquiond

57 papers A 3B 8C 7Misc 1Journal 25Unranked 8

Year	Rank	Type	Title / Venue / Authors
2026	B	`conf`	Certifying the Decidability of the Word Problem in Monoids at Large. CPP Reinis Cirpons, Florent Hivert, Assia Mahboubi, Guillaume Melquiond, James D. Mitchell, Finn Smith
2024	J	`jnl`	A Safe Low-Level Language for Computer Algebra and Its Formally Verified Compiler. Proc. ACM Program. Lang. Guillaume Melquiond, Josué Moreau
2024	B	`conf`	End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation. ITP Florian Faissole, Paul Geneau de Lamarlière, Guillaume Melquiond
2023	J	`jnl`	A strong call-by-need calculus. Log. Methods Comput. Sci. Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond
2023	J	`jnl`	Enabling Floating-Point Arithmetic in the Coq Proof Assistant. J. Autom. Reason. Érik Martin-Dorel, Guillaume Melquiond, Pierre Roux
2023	J	`jnl`	Floating-point arithmetic. Acta Numer. Sylvie Boldo, Claude-Pierre Jeannerod, Guillaume Melquiond, Jean-Michel Muller
2023	C	`conf`	Slimmer Formal Proofs for Mathematical Libraries. ARITH Paul Geneau de Lamarlière, Guillaume Melquiond, Florian Faissole
2023	J	`jnl`	WhyMP, a formally verified arbitrary-precision integer library. J. Symb. Comput. Guillaume Melquiond, Raphaël Rieu-Helft
2021	B	`conf`	A Strong Call-By-Need Calculus. FSCD Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond
2021	J	`jnl`	A strong call-by-need calculus. CoRR Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond
2021	—	`conf`	Plotting in a Formally Verified Way. F-IDE@NFM Guillaume Melquiond
2021	C	`conf`	Some Formal Tools for Computer Arithmetic: Flocq and Gappa. ARITH Sylvie Boldo, Guillaume Melquiond
2020	B	`conf`	WhyMP, a formally verified arbitrary-precision integer library. ISSAC Guillaume Melquiond, Raphaël Rieu-Helft
2019	—	`book`	Formal Verification for Numerical Computations, and the Other Way Around. Guillaume Melquiond
2019	C	`conf`	Formal Verification of a State-of-the-Art Integer Square Root. ARITH Guillaume Melquiond, Raphaël Rieu-Helft
2019	J	`jnl`	Formally Verified Approximations of Definite Integrals. J. Autom. Reason. Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
2018	A	`conf`	A Why3 Framework for Reflection Proofs and Its Application to GMP's Algorithms. IJCAR Guillaume Melquiond, Raphaël Rieu-Helft
2018	—	`book`	Handbook of Floating-Point Arithmetic (2nd Ed.). Jean-Michel Muller, Nicolas Brunie, Florent de Dinechin, Claude-Pierre Jeannerod, Mioara Joldes, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, Serge Torres
2017	—	`conf`	A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT. CAV (2) Sylvain Conchon, Mohamed Iguernelala, Kailiang Ji, Guillaume Melquiond, Clément Fumex
2017	—	`book`	Computer Arithmetic and Formal Proofs - Verifying Floating-point Algorithms with the Coq System. Sylvie Boldo, Guillaume Melquiond
2017	—	`conf`	How to Get an Efficient yet Verified Arbitrary-Precision Integer Library. VSTTE Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond
2016	J	`jnl`	Formalization of real analysis: a survey of proof assistants and libraries. Math. Struct. Comput. Sci. Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
2016	B	`conf`	Formally Verified Approximations of Definite Integrals. ITP Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
2016	J	`jnl`	Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq. J. Autom. Reason. Érik Martin-Dorel, Guillaume Melquiond
2015	J	`jnl`	Coquelicot: A User-Friendly Library of Real Analysis for Coq. Math. Comput. Sci. Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
2015	J	`jnl`	Verified Compilation of Floating-Point Computations. J. Autom. Reason. Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
2014	—	`conf`	Automating the Verification of Floating-Point Algorithms. SMT Guillaume Melquiond
2014	J	`jnl`	Trusting computations: A mechanized proof from partial differential equations to actual program. Comput. Math. Appl. Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2013	C	`conf`	A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. IEEE Symposium on Computer Arithmetic Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
2013	B	`conf`	Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus. IFM Daisuke Ishii, Guillaume Melquiond, Shin Nakajima
2013	J	`jnl`	Numerical approximation of The Masser-Gramain constant to four decimal digits: δ = 1.819.... Math. Comput. Guillaume Melquiond, W. Georg Nowak, Paul Zimmermann
2013	—	`conf`	Preserving User Proofs across Specification Changes. VSTTE François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich
2013	J	`jnl`	Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program. J. Autom. Reason. Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2012	A	`conf`	A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic. IJCAR François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond
2012	—	`conf`	Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers. SMT@IJCAR Sylvain Conchon, Guillaume Melquiond, Cody Roux, Mohamed Iguernelala
2012	J	`jnl`	Floating-point arithmetic in the Coq system. Inf. Comput. Guillaume Melquiond
2012	B	`conf`	Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives. CPP Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
2012	J	`jnl`	Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program. CoRR Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2011	J	`jnl`	Certifying the Floating-Point Implementation of an Elementary Function Using Gappa. IEEE Trans. Computers Florent de Dinechin, Christoph Quirin Lauter, Guillaume Melquiond
2011	C	`conf`	Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq. IEEE Symposium on Computer Arithmetic Sylvie Boldo, Guillaume Melquiond
2011	J	`jnl`	Wave Equation Numerical Resolution: Mathematics and Program CoRR Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2010	J	`jnl`	Certification of bounds on expressions involving rounded operators. ACM Trans. Math. Softw. Marc Daumas, Guillaume Melquiond
2010	B	`conf`	Formal Proof of a Wave Equation Resolution Scheme: The Method Error. ITP Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2010	J	`jnl`	Formal Proof of a Wave Equation Resolution Scheme: the Method Error CoRR Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2010	—	`book`	Handbook of Floating-Point Arithmetic. Jean-Michel Muller, Nicolas Brisebarre, Florent de Dinechin, Claude-Pierre Jeannerod, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, Damien Stehlé, Serge Torres
2009	—	`conf`	Combining Coq and Gappa for Certifying Floating-Point Programs. Calculemus/MKM Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond
2009	C	`conf`	IEEE Interval Standard Working Group - P1788: Current Status. IEEE Symposium on Computer Arithmetic William W. Edmonson, Guillaume Melquiond
2008	J	`jnl`	Certifying floating-point implementations using Gappa CoRR Florent de Dinechin, Christoph Quirin Lauter, Guillaume Melquiond
2008	J	`jnl`	Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd. IEEE Trans. Computers Sylvie Boldo, Guillaume Melquiond
2008	A	`conf`	Proving Bounds on Real-Valued Functions with Computations. IJCAR Guillaume Melquiond
2007	J	`jnl`	Certification of bounds on expressions involving rounded operators CoRR Marc Daumas, Guillaume Melquiond
2007	J	`jnl`	Formally certified floating-point filters for homogeneous geometric predicates. RAIRO Theor. Informatics Appl. Guillaume Melquiond, Sylvain Pion
2006	—	`conf`	A Proposal to add Interval Arithmetic to the C++ Standard Library. Reliable Implementation of Real Number Algorithms Sylvain Pion, Hervé Brönnimann, Guillaume Melquiond
2006	Misc	`conf`	Assisted verification of elementary functions using Gappa. SAC Florent de Dinechin, Christoph Quirin Lauter, Guillaume Melquiond
2006	—	`—`	De l'arithmétique d'intervalles à la certification de programmes. (From interval arithmetic to program verification). Guillaume Melquiond
2006	J	`jnl`	The design of the Boost interval arithmetic library. Theor. Comput. Sci. Hervé Brönnimann, Guillaume Melquiond, Sylvain Pion
2005	C	`conf`	Guaranteed Proofs Using Interval Arithmetic. IEEE Symposium on Computer Arithmetic Marc Daumas, Guillaume Melquiond, César A. Muñoz