Séminaire Philmath
Nous aurons le plaisir d’accueillir : Paolo Pistone (ENS, Lyon)
Titre : Proofs as Programs in the Era of Algorithmic Culture
Résumé : Historically, logic, and notably proof theory, have played an important role for understanding computation and programming. Still today, ideas and methods from logic and semantics are at the heart of the study of crucial problems in computer science, like verification (will the algorithm meet its own specification?) or program equivalence (do two algorithms compute the same function?).
Yet, computer science is a rapidly evolving field, and statistical inference methods have quickly gained a dominant position among programming paradigms. The algorithms arising from such methods are not thought to meet some specification exactly, but only up to some probability, nor to compute some given function precisely, but only to approximate its values in an efficient way. At the same time, also the philosophy and sociology of algorithms seem to have moved towards an image of computer science that is largely built over the pervasive role of statistical learning algorithms.
In view of these considerations, in this talk I will touch on a couple of troubling questions. What is the relevance, today, of the viewpoint on algorithms that arises from logic and proof theory? And more specifically, to which extent can the "Curry-Howard" correspondence between proofs and programs, focused on the image of algorithms as absolutely correct implementations of mathematical functions, account for algorithms whose correction is intrinsically approximated or probabilistic?
lien zoom :
https://pantheonsorbonne.zoom.us/j/91542712309?pwd=BMj0EHr1z2CVblnRzbRJVeZagdi1ND.1