6 Search Results for "Melquiond, Guillaume"

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.30
A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations

Authors: Sewon Park and Holger Thies

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

Abstract
In exact real computation real numbers are manipulated exactly without round-off errors, making it well-suited for high precision verified computation. In recent work we propose an axiomatic formalization of exact real computation in the Coq theorem prover. The formalization admits an extended extraction mechanism that lets us extract computational content from constructive parts of proofs to efficient programs built on top of AERN, a Haskell library for exact real computation. Many processes in science and engineering are modeled by ordinary differential equations (ODEs), and often safety-critical applications depend on computing their solutions correctly. The primary goal of the current work is to extend our framework to spaces of functions and to support computation of solutions to ODEs and other essential operators. In numerical mathematics, the most common way to represent continuous functions is to use polynomial approximations. This can be modeled by so-called Taylor models, that encode a function as a polynomial and a rigorous error-bound over some domain. We define types of classical functions that do not hold any computational content and formalize Taylor models to computationally approximate those classical functions. Classical functions are defined in a way to admit classical principles in their constructions and verification. We define various basic operations on Taylor models and verify their correctness based on the classical functions that they approximate. We then shift our interest to analytic functions as a generalization of Taylor models where polynomials are replaced by infinite power series. We use the formalization to develop a theory of non-linear polynomial ODEs. From the proofs we can extract certified exact real computation programs that compute solutions of ODEs on some time interval up to any precision.
Cite as

Sewon Park and Holger Thies. A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{park_et_al:LIPIcs.ITP.2024.30,
  author =	{Park, Sewon and Thies, Holger},
  title =	{{A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{30:1--30:19},
  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.30},
  URN =		{urn:nbn:de:0030-drops-207581},
  doi =		{10.4230/LIPIcs.ITP.2024.30},
  annote =	{Keywords: Exact real computation, Taylor models, Analytic functions, Computable analysis, Program extraction}
}
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/LIPIcs.ITP.2019.7
Primitive Floats in Coq

Authors: Guillaume Bertholon, Érik Martin-Dorel, and Pierre Roux

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
Some mathematical proofs involve intensive computations, for instance: the four-color theorem, Hales' theorem on sphere packing (formerly known as the Kepler conjecture) or interval arithmetic. For numerical computations, floating-point arithmetic enjoys widespread usage thanks to its efficiency, despite the introduction of rounding errors. Formal guarantees can be obtained on floating-point algorithms based on the IEEE 754 standard, which precisely specifies floating-point arithmetic and its rounding modes, and a proof assistant such as Coq, that enjoys efficient computation capabilities. Coq offers machine integers, however floating-point arithmetic still needed to be emulated using these integers. A modified version of Coq is presented that enables using the machine floating-point operators. The main obstacles to such an implementation and its soundness are discussed. Benchmarks show potential performance gains of two orders of magnitude.
Cite as

Guillaume Bertholon, Érik Martin-Dorel, and Pierre Roux. Primitive Floats in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bertholon_et_al:LIPIcs.ITP.2019.7,
  author =	{Bertholon, Guillaume and Martin-Dorel, \'{E}rik and Roux, Pierre},
  title =	{{Primitive Floats in Coq}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{7:1--7:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.7},
  URN =		{urn:nbn:de:0030-drops-110629},
  doi =		{10.4230/LIPIcs.ITP.2019.7},
  annote =	{Keywords: Coq formal proofs, floating-point arithmetic, reflexive tactics, Cholesky decomposition}
}
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}
}
  • Refine by Author
  • 4 Melquiond, Guillaume
  • 2 Geneau de Lamarlière, Paul
  • 1 Balabonski, Thibaut
  • 1 Bertholon, Guillaume
  • 1 Brönnimann, Hervé
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 2 floating-point arithmetic
  • 1 Analytic functions
  • 1 C++
  • 1 Cholesky decomposition
  • 1 Computable analysis
  • Show More...

  • Refine by Type
  • 5 document
  • 1 artifact

  • Refine by Publication Year
  • 3 2024
  • 1 2006
  • 1 2019
  • 1 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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