Paolo Pistone: Logic and Approximate Computation: a Marriage of Interest?

Organized by the Department of Logic

Further information

Invitation pdf

Paolo Pistone (Università Roma Tre):
Logic and Approximate Computation: a Marriage of Interest?

Abstract
Logic has historically played a fundamental 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 several programming paradigms today focus on algorithms which 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. A natural question is thus whether proof systems and semantical methods, originally conceived to answer qualitative (i.e. yes/no) questions, can still play a role in answering more quantitative questions, that is, to measure the accuracy of approximate algorithms. In this talk I will present a few ideas and results suggesting that some well-known approaches relating logic and computer science (like the Curry-Howard correspondence or the realizability interpretation) can indeed also account for programs whose correction is intrinsically approximated or probabilistic.