From Implicit Complexity to Quantitative Resource Analysis
PhD Open, University of Warsaw
June 2015

Is it possible to automatically evaluate the time complexity of any functional program? How far could one go, given the intrinsic limitations imposed by computability theory? Giving an answer to the questions above, even a partial one, would be beneficial in any context in which programs with too-high time complexity are harmful (or should simply ruled out from the game), like in security and cryptography. In this course, we will show how to the problems above can be approached by first characterizing relatively small time complexity classes by simple, paradigmatic programming languages, then turning the latter into formal methods. We will do that (at least) for term rewrite systems and the lambda-calculus.

[1] U. Dal Lago. A Short Introduction to Implicit Computational Complexity. ESSLLI 2010 Lecture Notes, 2010. [pdf]
Teaching Material
Slides, Part I (27/6/2015) [ pdf ]
Slides, Part II (27/6/2015) [ pdf ]
Slides, Part III (27/6/2015) [ pdf ]
Written Assignment [ pdf ]