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.
Summary
Implicit Complexity at a Glance
Playing with Computational Models
Implicit Complexity in Function Algebras
Implicit Complexity in Functional Programs
Implicit Complexity in the Lambda Calculus
Complexity Analysis by Program Transformation
Bounded Linear Logic and Linear Dependency
Schedule
Thursday, June 25th, 2015: 14.45-15.45
Thursday, June 25th, 2015: 17.30-19.30
Friday, June 26th: 2015: 14.15-15.45
Friday, June 26th, 2014: 16.15-17.15
Saturday, June 27th: 2015: 10.00-11.30
Saturday, June 27th, 2014: 12.00-13.00
References
[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 ] Assignments
Written Assignment [ pdf ]