| Title: |
Machine-Checked Computational Mathematics (Invited Talk) |
| Authors: |
Mahboubi, Assia |
| Contributors: |
Assia Mahboubi |
| Publisher Information: |
Schloss Dagstuhl – Leibniz-Zentrum für Informatik |
| Publication Year: |
2023 |
| Collection: |
DROPS - Dagstuhl Research Online Publication Server (Schloss Dagstuhl - Leibniz Center for Informatics ) |
| Subject Terms: |
Type theory; computer algebra; interactive theorem proving |
| Description: |
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. |
| Document Type: |
article in journal/newspaper; conference object |
| File Description: |
application/pdf |
| Language: |
English |
| Relation: |
Is Part Of LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023); https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.5 |
| DOI: |
10.4230/LIPIcs.CALCO.2023.5 |
| Availability: |
https://doi.org/10.4230/LIPIcs.CALCO.2023.5; https://nbn-resolving.org/urn:nbn:de:0030-drops-188024; https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.5 |
| Rights: |
https://creativecommons.org/licenses/by/4.0/legalcode |
| Accession Number: |
edsbas.7BABD4D7 |
| Database: |
BASE |