DS0705 - Fondements du numérique

Expanding Logical Ideas for Complexity Analysis – ELICA

Submission summary

Static complexity analysis aims at providing methods for determining how many computational resources (time units, memory cells) will be required by a program for its execution. Although this task subsumes, in general, a well known undecidable problem, it is possible to devise sound methods covering a large number of cases, including, if possible, those found in practice.
The aim of the ELICA project is to develop logical methods for static complexity analysis, improve their expressiveness and extend their application to non-deterministic and concurrent programming paradigms.
Logic-based tools, in particular of proof theoretic origin, have proved to be of capital importance for static complexity analysis. Criteria guaranteeing complexity bounds have been formulated (some by prospective participants to the ELICA project) using structural restrictions of the lambda-calculus, subsystems of linear logic in which cut-elimination has a limited complexity, type systems for functional languages, and semantic methods (polynomial interpretations and denotational semantics). These methods do not give precise bounds on the complexity of programs, but they have the advantage of being modular and of producing easily verifiable certificates.
However, these methods currently apply only to a restricted range of programming languages, mostly of functional nature. Even in the functional case, the criteria are unsatisfactory in terms of expressiveness, i.e., with respect to the number of practical programs to which they can be applied. The ELICA project fixes as objective the development of extant logical methods and the introduction of new ones, in order to:
- improve the expressiveness of static complexity analysis criteria for first-order functional languages, but above all extend the scope of such criteria to higher-order complexity (in particular, type-2 complexity), which is still largely unexplored;
- increase the practical impact of these methods by defining complexity criteria for languages with imperative features, and relate them to the criteria for the verification of security properties (such as non-interference);
- apply these methods to non-deterministic and probabilistic languages, to analyze the complexity of programs implementing randomized algorithms, with the long-term goal of employing such methods for the analysis of cryptographic and security protocols;
- extend the scope of these methods to the analysis of concurrent systems. Here, the problem is above all of foundational nature, because there currently is no general definition of computational complexity for concurrent processes. We therefore propose to first develop a theory of computational complexity of interactive behaviors (generalizing problems and functions), capable of giving a formal content to notions such as answer time to a request, memory space, number of active processes, etc. Subsequently, we will study the application of logical methods to this theory.

Project coordination

Damiano Mazza (Laboratoire d'Informatique de Paris Nord)

The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.

Partner

LIPN Laboratoire d'Informatique de Paris Nord
LIP Laboratoire de l'Informatique du Parallélisme
Inria Institut de Recherche en Informatique et en Automatique

Help of the ANR 398,528 euros
Beginning and duration of the scientific project: September 2014 - 48 Months

Useful links

Explorez notre base de projets financés

 

 

ANR makes available its datasets on funded projects, click here to find more.

Sign up for the latest news:
Subscribe to our newsletter