L'Agence nationale de la recherche Des projets pour la science

Translate this page in english

Blanc (BLANC) 2008
Projet COMPLICE

Complexité Implicite, Concurrence et Extraction

Le champ de recherche de ce projet est motivé par la perspective de développer des concepts et des outils fondamentaux pour raisonner sur les prorpiétés relatives aux ressources des logiciels ou des systèmes. L'approche proposée est celle de la complexité implicite (CI), qui étudie des calculs et des langages pour la programmation à complexité bornée, par exemple des langages pour lesquels tous les programmes sont par construction de complexité Ptime (terminant en temps polynomial par rapport à la taille de l'entrée). La CI a été étudiée depuis le début des années 90, en partant d'approches basées sur la logique, la théorie de la récursion et la programmation fonctionnelle. Plusieurs disciplines de programmation ont été données dans ces langages, basées par exemple sur des restrictions des schémas de récursion ou des règles logiques, et qui permettent de caractériser des classes de complexité comme Ptime, ou Pspace (travaux de Leivant, Jones, Girard, Marion). Les techniques utilisées sont par exemple la logique linéaire, les systèmes de types, les interprétations, les ordres de terminaison... Ce projet explorera différentes branches de la CI. D'un côté il cherchera à approfondir notre connaissance des fondements sémantiques et logiques de la CI, en particulier par la logique linéaire. Il étudiera aussi les manières de certifier la complexité des programmes fonctionnels et cherchera à améliorer les propriétés des critères disponibles dans ce domaine (en particulier basés sur la méthode des quasi-interprétations). Par ailleurs ce projet explorera l'extension du champ de la complexité implicite à de nouveaux domaines: d'un côté l'extraction à partir de preuves formelles de programmes à complexité bornée, de l'autre la mise au point de critères de CI pour les systèmes concurrents, dans le cadre des calculs de processus (comme le pi-calcul). Dans le premier domaine cité, l'idée est de définir des systèmes de preuves avec la propriété suivante: en construisant une preuve établissant la totalité d'une fonction définie par une spécification, on peut dans un deuxième temps, en extraire un programme implémentant la spécification et certifié de complexité Ptime. Dans le deuxième domaine, celui des systèmes concurrents, nous souhaitons définir des méthodes similaires à celles déjà disponibles pour les programmes fonctionnels, permettant de certifier statiquement pour un système donné des bornes sur l'usage des ressources, comme par exemple sur le temps d'exécution ou le nombre et la taille des processus. . Enfin le projet étudiera aussi l'utilisation de la CI pour caractériser des classes de complexité parallèles comme par exemple NC, la classe des algorthmes parallélisables de façon efficace.

Partenaires

 ECOLE NORMALE SUPERIEURE DE LYON

 INSTITUT NATIONAL POLYTECHNIQUE DE LORRAINE

 UNIVERSITE DE PARIS XIII

Aide de l'ANR 299 766 euros
Début et durée du projet scientifique - 48 mois

 

Programme ANR : Blanc (BLANC) 2008

Référence projet : ANR-08-BLAN-0211

Coordinateur du projet :
ECOLE NORMALE SUPERIEURE DE LYON (ECOLE NORMALE SUPERIEURE DE LYON)

 

Revenir à la page précédente

 

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.