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 ]