15 juin 2022
Le Bois-Marie
Fuseau horaire Europe/Paris

Verified Computational Mathematics (T: 45min + Q: 15min)

15 juin 2022, 14:30
1h
Centre de conférences Marilyn et James Simons (Le Bois-Marie)

Centre de conférences Marilyn et James Simons

Le Bois-Marie

35, route de Chartres 91440 Bures-sur-Yvette

Orateur

Prof. Assia MAHBOUBI (INRIA)

Description

Computers are widely used as observation instruments for testing and refining conjectures, in a broad range of mathematical areas. They actually even substantiate actual proof steps in published proofs. In particular, a large class of computer proofs today involve symbolic computations, often produced by computer algebra systems. While these systems have become amazingly efficient, they also tend to exhibit awkward behaviors on seemingly innocuous queries. This talk will discuss the challenges raised by the formal verification of symbolic computation, and the potential of proof assistants based on dependent types.

Documents de présentation

Aucun document.