CR 13: Implicit Computational Complexity (2015-2016)

Friday 1:30pm - 3:30pm in room B1


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.


Lecture 1

Lecture 2

Lecture 3

Lecture 4

Lecture 5

Lecture 6

Lecture 7

  1. Intuitionistic logic and lambda-calculus
  2. Elementary linear logic

Lecture 8

  1. Elementary linear logic (continued)

Lecture 9

  1. Elementary linear logic (continued)

Lecture 10

  1. Elementary linear logic (continued)
  2. Light linear logic

Lecture 11

  1. Light linear logic (continued)





Main evaluation will be a final exam.

Additional evaluation (leading to bonus on the final grade) will be based on homework.