Implicit Complexity and the Curry-Howard Correspondence
Days in Logic 2016, University of Lisbon

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.

[1] U. Dal Lago. A Short Introduction to Implicit Computational Complexity. ESSLLI 2010 Lecture Notes, 2010. [pdf]