Logic is widely used to analyse the correctness of programs. But on the quantitative side, can it say anything about their efficiency?
In this course we will take an abstract view on this question, through the approach of complexity. We will first present a logic which is well-suited to study quantitative properties, as it gives an explicit status to duplication and erasing: linear logic. In a second part of the course we will show how this logic leads to the design of type systems for functional calculi, which statically ensure complexity properties, e.g.: if a program is well-typed then it runs in polynomial time.
Main evaluation will be a final exam.
Additional evaluation (leading to bonus on the final grade) will be based on homework.