Abstract:

Rice's Theorem is a cornerstone of classical computability. Like other  classical results, it is extensional: it concern the behaviour of  partial recursive functions rather than the programs computing them.  However, program analysis is interested in the behaviour of programs: we  don't just want to know what the program does but also how it works.

The goal of this talk is to present generalised versions of Rice's  Theorem and demonstrate how they can be applied to study intensional  properties such as time and space complexity. We obtain simple proofs of  several striking negative results about overapproximations of  intensional properties. For example that any decidable set of programs  that contains the set of polytime programs must contain programs of  arbitrarily high time complexity.

Biosketch:

Jean-Yves Moyen is Associate Professor at University Paris 13, and   currently Marie Curie fellow at University of Copenhagen. His principal   focus is the field of Implicit Computational Complexity that aims at   finding program analysis to guarantee complexity bounds. He is more generally interested in Program Analysis, Computability, and Logic.