TITLE: IMPLICIT COMPLEXITY AND THE CURRY-HOWARD CORRESPONDENCE
ABSTRACT:
The Curry-Howard Correspondence tells us that proofs behave as
programs and formulas act as types. This enabled in the last fifty
years a lot of interaction between proof theory and theoretical
computer science. Implicit computational complexity, on the other
hand, looks for characterizations of complexity classes from
programming language theory and mathematical logic. This course starts
with a brief overview of the two disciplines, then showing how they
have fruitfully interacted in the last thirty years. Some time will
be spent, in particular, in describing how techniques from
Girard's linear logic can be applied in this context.