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)

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

- Application to complexity
- elementary linear logic and exponential complexity classes
- light linear logic and polynomial time complexity
- linear type systems: types for non-size-increasing computation, linear dependent types

- Proofs and Types
*(introduction to proof theory and λ-calculus)* - 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)
- A Syntactical Analysis of Non-Size-Increasing Polynomial Time Computation (Klaus Aehlig and Helmut Schwichtenberg)

- 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**.