Back

Implicit Computational Complexity

Daniel Leivant
Section: Computation
Level: Advanced

Description

The main topic of this course is to present recent advances on analysis of the computational complexity of (functional) programs, that we call Implicit Computational Complexity (ICC). ICC is based on ramified type systems and proof theoretic approaches.

In addition, we shall discuss about 'functions versus algorithms' and of intensionality. From then on, we shall see that ICC may have some applications to efficient compilation, in particular, on first order functional programming based on rewrite rules.

The materials come from works of Bellantoni, Colson, Cook, Jones, Hofmann, Leivant, Girard, Niggl, and Schwichtenberg, ...

Prerequisites

Some backgrounds on computational complexity, functional programming and proof theory.

Materials

PDFabstract

Lecturer

Daniel Leivant
http://www.cs.indiana.edu/~leivant