Implicit Computational Complexity

Implicit Computational Complexity (ICC) has emerged from various propositions to use logic and formal methods like types, rewriting systems, interpretations... to provide languages for complexity-bounded computation, in particular for polynomial time computing.

It aims at studying the computational complexity of programs without refering to a particular machine model and explicit bounds on time or memory, but instead by relying on programming or logical disciplines that imply complexity properties. Several approaches have been explored for that purpose, like restrictions on primitive recursion, lambda calculus, types, linear logic, rewriting systems .... They originally mostly came from the functional programming paradigm, but imperative programming is now also addressed. Two objectives of ICC are:

  • on the one hand to find natural implicit logical characterizations of functions of various complexity classes,
  • on the other hand to design criteria usable for the static verification of programs complexity. In particular the latter goal requires characterizations which are flexible enough to validate commonly used algorithms.

Finding out more

The home page of this workshop supported by the NO-CoST ANR project is online.