LIPIcs.CALCO.2023.5.pdf
- Filesize: 328 kB
- 1 pages
Document
Machine-Checked Computational Mathematics (Invited Talk)
Author
Assia Mahboubi 
-
Part of:
Volume:
10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Conference on Algebra and Coalgebra in Computer Science (CALCO) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-09-02
File
Document Identifiers
Author Details
Cite As Get BibTex
Assia Mahboubi. Machine-Checked Computational Mathematics (Invited Talk). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, p. 5:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CALCO.2023.5
Abstract
This talk shall discuss the potential impact of formal methods, and in particular, of interactive theorem proving, on computational mathematics. Geared with increasingly fast computer algebra libraries and scientific computing software, computers have become amazing instruments for mathematical guesswork. In fact, computer calculations are even sometimes used to substantiate actual reasoning steps in proofs, later published in major venues of the mathematical literature. Yet surprisingly, little of the now standard techniques available today for verifying critical software (e.g., cryptographic components, airborne commands, etc.) have been applied to the programs used to produce mathematics. In this talk, we propose to discuss this state of affairs.
Subject Classification
ACM Subject Classification
- Computing methodologies → Theorem proving algorithms
- Theory of computation → Type theory
Keywords
- Type theory
- computer algebra
- interactive theorem proving
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads