Implicit Complexity
Caleidoscope Summer School
June 2019, Paris, France
The aim of implicit computational complexity (ICC in the following) is the one of giving machine-free characterisations of complexity classes based on tools from mathematical logic, and in particular from proof theory and recursion theory. This three-hour tutorial on the subject does not aim to be an exhaustive description of the field, which has developed quite substantially in the last thirty years. Rather, after giving a bird-eye view on the subject, I will focus on some themes which have been among the central ones in ICC lately, namely the characterisation of complexity classes through the Curry-Howard correspondence, the problem of intentional expressivity of ICC systems, and some new challenges ICC is facing nowadays, in particular related to probabilistic and concurrent computation.

Course Synopsis