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, ...
Some backgrounds on computational complexity, functional programming and proof theory.