# CR 13: Implicit Computational Complexity (2015-2016)

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

## Description

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 6

• References:
• Homework: (return date: November 6th) read the notes as an article, write down detailed proofs, find possible places where important details are missing (at least from your point of view), give remarks, comments, optimizations, etc and send all that.

## Lecture 7

1. Intuitionistic logic and lambda-calculus
• Sequent calculus LJ2 and decoration with lambda-terms.
• Properties of cut-elimination and beta-reduction.
• Data-types: N, W.
• Iteration on Church integers and Church binary words.
• Strong normalisation of typable terms.
2. Elementary linear logic
• Language and sequent calculus rules.
• Intuitionistic version IELL and decoration with lambda-terms.
• Forgetful map to LJ2.
• Affine version IEAL.
• Data-types: NIELL, WIELL.

## Lecture 8

1. Elementary linear logic (continued)
• Examples of terms typed in IEAL: addition, multiplication, word concatenation, ...
• ELL proof-nets and their reduction.
• Complexity bound on the reduction of ELL proof-nets, in O(2d|R|). Beginning of the proof.

## Lecture 9

1. Elementary linear logic (continued)
• Complexity bound on the reduction of ELL proof-nets: end of the proof.
• The functions representable in IEAL with types (N-o!kN) are exactly the elementary functions.
• Iteration in IEAL.
• Functions representable in IELL with type (!W-o!!Bool) are polynomial time predicates.

## Lecture 10

1. Elementary linear logic (continued)
• Functions representable in IELL with type (!W-o!3Bool) are exponential time predicates.
2. Light linear logic
• Intuitionistic version ILLL and decoration with lambda-terms. Forgetful map to IELL. Affine version ILAL.
• Data types NILLL, WILLL. Examples of typed terms.
• Iteration.
• LLL proof-nets and their reduction. Complexity bound on the reduction of LLL proof-nets, in O(|R|2d). Beginning of the proof.

## Lecture 11

1. Light linear logic (continued)
• Complexity bound on the reduction of LLL proof-nets: end of the proof.
• Data-types coercions.
• FP completeness (proof sketch).
• The functions representable in ILAL with types (W-o§kW) are exactly the class FP.
• Subsystem DLAL: polynomial bound on beta reduction.

## Content

• 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

## Prerequisites

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

## Evaluation

Main evaluation will be a final exam.

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