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.
Summary
Introduction to Implicit Complexity
A Bird's Eye View on the Curry-Howard Correspondence
Characterizing Complexity Classes by Logics and Types
Schedule
Thursday, January 28th, 2016: 10:00-11.00
Friday, January 29th: 2016: 10.30-11.30
Saturday, January 30th, 2016: 9.00-10.00
References
[1]
U. Dal Lago.
A Short Introduction to Implicit Computational Complexity. ESSLLI 2010 Lecture Notes, 2010. [pdf]