Résumé

The motivation for this project is to develop fondamental concepts and tools to reason about resource-related properties of software and computational systems. The approach followed is that of implicit computational complexity (ICC), which studies calculi and programming languages for complexity-bounded computation, for instance languages in which all programs are by construction of complexity Ptime (polynomial time w.r.t. the size of the input). ICC has been developed since the early 90s, starting from approaches in logic, recursion theory and functional programming. Various disciplines have been given in these calculi, based for instance on restrictions of recursion schemes or logical rules, and which allow to characterize complexity classes like Ptime, Pspace (e.g. work by Leivant, Jones, Girard, Marion) Typical techniques used are linear logic, type systems, interpretations, termination orderings...

This project will investigate several directions of ICC. On the one hand it will deepen the semantical and logical foundations of ICC, in particular in linear logic. It will study how to certify the complexity of functional programs and will improve the criteria available in this area (in particular based on quasi-interpretations).

Moreover it will explore the extension of ICC to two new areas : extraction from formal proofs of complexity-bounded programs on the one hand, and design of ICC criteria for concurrent systems in the setting of process calculi, on the other.

In the first area, the idea is to define proof-systems such that after constructing a proof establishing the totality of a function defined by a specification, one can extract from the proof a program implementing the specification and certified of Ptime complexity.

In the second area, concurrent systems, we would like to define techniques similar to those of the functional setting, allowing to certify statically for a system some bounds on the usage of resources, like its running time or its number of processes.

Finally the project will also study the usage of ICC for characterizing parallel complexity classes like NC, the class of efficiently parallelizable algorithms.