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.

- Patrick Baillot (Complexity)
- Olivier Laurent (Linear Logic)

**References:****Homework:**Subject 1: Classical Sequent Calculus (return date:*September 19th*)

**References:**- Théorie de la démonstration (pages 19-25 and 85-86)
- Introduction to Linear Logic (pages 90-130 = slides 33-45)

**Homework:**Subject 2: Linear Sequent Calculus (return date:*September 26th*)

**References:**Théorie de la démonstration (pages 85-90)

**References:**- An Introduction to Proof Nets (pages 1-13)
- Théorie de la démonstration (pages 95-99 and 103-104)

**Homework:**Subject 3: Multiplicative Proof-Nets (return date:*October 10th*)

**References:**- An Introduction to Proof Nets (pages 15-22)
- Théorie de la démonstration (pages 106-112)

**Preparation:**

- Linear Logic
- its proof systems: sequent calculus, proof-nets, cut-elimination
- analysis of intuitionistic logic and lambda-calculus

- Application to complexity
- elementary linear logic and exponential complexity classes
- light linear logic and polynomial time complexity

- Interactive tutorial on sequent calculus
- Proofs and Types
*(introduction to proof theory and λ-calculus)* - Linear Logic school 2016
*(another course on linear logic)* - Théorie de la démonstration / Proof Theory
*(course notes in French)* - An Introduction to Proof Nets
*(preliminary course notes)* - Decorating Proof-Nets with Lambda-Terms
*(notes on the relation between proof-nets and the λ-calculus)* - Linear Logic
*(J.-Y. Girard's original paper)* - LL Wiki
*(wiki on Linear Logic)* - Light Linear Logic (Jean-Yves Girard)
- Intuitionistic light affine logic (Andrea Asperti and Luca Roversi)
- On the expressivity of elementary linear logic: Characterizing Ptime and an exponential time hierarchy (Patrick Baillot)

- Simply typed lambda-calculus
- Bases of natural deduction and sequent calculus

Main evaluation will be a **final exam**.

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