Search Results

Documents authored by Melquiond, Guillaume

Document
DOI: 10.4230/LIPIcs.ITP.2026.9
Functional Correctness of an Optimized Modular Inversion Algorithm

Authors: Assia Mahboubi, Guillaume Melquiond, Pierre-Yves Strub, and Tomás Vallejos Parada

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
This article describes the first mechanized proof of functional correctness of an algorithm due to Pornin (2020), for computing modular inverses via an optimized extended binary GCD algorithm. This algorithm is widely used in cryptography applications, due to its speed and constant-timeness. But this speed comes from the use of approximate computations during its loop iterations. In particular, the pen-and-paper proof of the fact that sufficiently many loop iterations were performed is especially intricate (and the originally published version was actually wrong), which negatively impacts the trust in the applications that rely on the algorithm. In this work, we expand the notes provided in the original description by Pornin into a complete formal proof. We discuss the challenges raised by its mechanization, which eventually relies on the collaboration of deductive program verification and interactive theorem proving through the use of the tools Rocq and Why3.
Cite as

Assia Mahboubi, Guillaume Melquiond, Pierre-Yves Strub, and Tomás Vallejos Parada. Functional Correctness of an Optimized Modular Inversion Algorithm. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{mahboubi_et_al:LIPIcs.ITP.2026.9,
  author =	{Mahboubi, Assia and Melquiond, Guillaume and Strub, Pierre-Yves and Vallejos Parada, Tom\'{a}s},
  title =	{{Functional Correctness of an Optimized Modular Inversion Algorithm}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{9:1--9:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.9},
  URN =		{urn:nbn:de:0030-drops-269839},
  doi =		{10.4230/LIPIcs.ITP.2026.9},
  annote =	{Keywords: deductive program verification, modular inversion algorithm, formal verification, Rocq, Why3}
}
Artifact
Software
DOI: 10.4230/artifacts.22454
CoqInterval

Authors: Paul Geneau de Lamarlière and Guillaume Melquiond

Abstract
Cite as

Paul Geneau de Lamarlière, Guillaume Melquiond. CoqInterval (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22454,
   title = {{CoqInterval}}, 
   author = {Geneau de Lamarli\`{e}re, Paul and Melquiond, Guillaume},
   note = {Software, version 4.10.0., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:78da3e6e98b7ef018180119255ce1e10a048cc88;origin=https://gitlab.inria.fr/coqinterval/interval.git;visit=swh:1:snp:c1aa8c7d68f6002ef304d4d2ea6f5170da9efb39}{\texttt{swh:1:dir:78da3e6e98b7ef018180119255ce1e10a048cc88}} (visited on 2024-11-28)},
   url = {https://gitlab.inria.fr/coqinterval/interval.git},
   doi = {10.4230/artifacts.22454},
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.14
End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation

Authors: Florian Faissole, Paul Geneau de Lamarlière, and Guillaume Melquiond

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
Designing an efficient yet accurate floating-point approximation of a mathematical function is an intricate and error-prone process. This warrants the use of formal methods, especially formal proof, to achieve some degree of confidence in the implementation. Unfortunately, the lack of automation or its poor interplay with the more manual parts of the proof makes it way too costly in practice. This article revisits the issue by proposing a methodology and some dedicated automation, and applies them to the use case of a faithful binary64 approximation of exponential. The peculiarity of this use case is that the target of the formal verification is not a simple modeling of an external code; it is an actual floating-point function defined in the logic of the Coq proof assistant, which is thus usable inside proofs once its correctness has been fully verified. This function presents all the attributes of a state-of-the-art implementation: bit-level manipulations, large tables of constants, obscure floating-point transformations, exceptional values, etc. This function has been integrated into the proof strategies of the CoqInterval library, bringing a 20× speedup with respect to the previous implementation.
Cite as

Florian Faissole, Paul Geneau de Lamarlière, and Guillaume Melquiond. End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{faissole_et_al:LIPIcs.ITP.2024.14,
  author =	{Faissole, Florian and Geneau de Lamarli\`{e}re, Paul and Melquiond, Guillaume},
  title =	{{End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.14},
  URN =		{urn:nbn:de:0030-drops-207420},
  doi =		{10.4230/LIPIcs.ITP.2024.14},
  annote =	{Keywords: Program verification, floating-point arithmetic, formal proof, automated reasoning, mathematical library}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.9
A Strong Call-By-Need Calculus

Authors: Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
We present a call-by-need λ-calculus that enables strong reduction (that is, reduction inside the body of abstractions) and guarantees that arguments are only evaluated if needed and at most once. This calculus uses explicit substitutions and subsumes the existing strong-call-by-need strategy, but allows for more reduction sequences, and often shorter ones, while preserving the neededness. The calculus is shown to be normalizing in a strong sense: Whenever a λ-term t admits a normal form n in the λ-calculus, then any reduction sequence from t in the calculus eventually reaches a representative of the normal form n. We also exhibit a restriction of this calculus that has the diamond property and that only performs reduction sequences of minimal length, which makes it systematically better than the existing strategy. We have used the Abella proof assistant to formalize part of this calculus, and discuss how this experiment affected its design.
Cite as

Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond. A Strong Call-By-Need Calculus. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 9:1-9:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{balabonski_et_al:LIPIcs.FSCD.2021.9,
  author =	{Balabonski, Thibaut and Lanco, Antoine and Melquiond, Guillaume},
  title =	{{A Strong Call-By-Need Calculus}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{9:1--9:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.9},
  URN =		{urn:nbn:de:0030-drops-142477},
  doi =		{10.4230/LIPIcs.FSCD.2021.9},
  annote =	{Keywords: strong reduction, call-by-need, evaluation strategy, normalization}
}
Document
DOI: 10.4230/DagSemProc.06021.4
A Proposal to add Interval Arithmetic to the C++ Standard Library

Authors: Sylvain Pion, Hervé Brönnimann, and Guillaume Melquiond

Published in: Dagstuhl Seminar Proceedings, Volume 6021, Reliable Implementation of Real Number Algorithms: Theory and Practice (2006)

Abstract
I will report on a recent effort by Guillaume Melquiond, Hervé Br"onnimann and myself to push forward a proposal to include interval arithmetic in the next C++ ISO standard. The goals of the standardization are to produce a unified specification which will serve as many uses of intervals as possible, together with hoping for very efficient implementations, closer to the compilers. I will describe how the standardization process works, explain some of the design choices made, and list some of the other questions arising in the process. We welcome any comment on the proposal.
Cite as

Sylvain Pion, Hervé Brönnimann, and Guillaume Melquiond. A Proposal to add Interval Arithmetic to the C++ Standard Library. In Reliable Implementation of Real Number Algorithms: Theory and Practice. Dagstuhl Seminar Proceedings, Volume 6021, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{pion_et_al:DagSemProc.06021.4,
  author =	{Pion, Sylvain and Br\"{o}nnimann, Herv\'{e} and Melquiond, Guillaume},
  title =	{{A Proposal to add Interval Arithmetic to the C++ Standard Library}},
  booktitle =	{Reliable Implementation of Real Number Algorithms: Theory and Practice},
  pages =	{1--25},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6021},
  editor =	{Peter Hertling and Christoph M. Hoffmann and Wolfram Luther and Nathalie Revol},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06021.4},
  URN =		{urn:nbn:de:0030-drops-7189},
  doi =		{10.4230/DagSemProc.06021.4},
  annote =	{Keywords: Interval arithmetic, C++, ISO standard}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact