2017/2018 Edition

From Implicit Complexity to Quantitative Resource Analysis

Lecturer: Ugo Dal Lago (University of Bologna, Italy).

About the lecturer | Course Summary | Slides: 1 2 3 | Assignment

About the lecturer: Ugo Dal Lago is an Assistant Professor in Computer Science at the University of Bologna. He received his Ph.D. from the same institution in 2006, and visited the universities of Verona and Paris VII as a postdoc in 2006 and 2007. During his thesis, Dal Lago received the IEEE Kleene Award for the best student paper presented at LICS, and the the IC-EATCS Award for the best Ph.D. thesis in theoretical computer science, both in 2006. Dal Lago is conducting research in implicit computational complexity and probabilistic computation, with special emphasis on higher-order aspects. He has published more than 60 papers in international conferences and journals, and served as program committee member in LICS, ICALP, FoSSaCS, and other well-respected conferences. He currently serves as a secretary of IFIP Working Group 1.6 on Term Rewriting, and is a member of the TLCA steering committee.

Course summary: 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.

Assignment: You can find the problem set here. Please send your solutions by Saturday, August 15.