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

Translate this page in english

Blanc International II - SIMI 2 - Science informatique et applications (Blanc Inter II SIMI 2) 2011
Projet Locali

Approche Logique de Nouveaux Paradigmes de Calcul

La logique et la théorie des algorithmes sont deux domaines clés en informatique. La logique est traditionnellement vue en Europe comme la clé de voûte de l'édifice mathématique, alors que les lettrés Chinois ont une tradition plus marquée en algorithmique. Les célèbres "Neufs chapitres sur les algorithmes" de la Chine ancienne et les théorie de la démonstration mécanique du mathématicien Wu Wenjun sont deux incarnations de cette tradition de la philosophie chinoise. Le dialogue entre la logique et la théorie des algorithmes a été une source constante de progrès pour les deux disciplines, progrès qui stimulent le développement de l'informatique.

Ce dialogue présente deux aspects : le premier se focalise sur les langages utilisés pour exprimer les démonstrations et les algorithmes. L'interprétation algorithmique des démonstration, permet d'utiliser des langages algorithmiques comme des langages de preuve, c'est-à-dire, d'importer des langages algorithmiques en logique. Il fournit, de manière duale, de nouveaux langages à la théorie des algorithmes. Un autre aspect de ce dialogue est le défi de prendre en compte la concurrences dans les modèles de calcul. Cette dualité se reflète dans l'opposition entre lambda-calcul et pi-calcul. Notre projet est d'étendre et de reformuler ces deux calculs et de proposer, par une analyse logique, de nouveaux langages de programmation et de nouveaux systèmes de preuve.

Les recherches de ce projet se focalisent sur de nouvelles directions qui émergent de ce dialogue entre la logique et la théorie des algorithmes : le calcul des schémas, une nouvelle manière d'exprimer les théories en déduction modulo polarisée clausale, une nouvelle extension des automates d'arbres, CCTS, qui permet une communication interne et une composition parallèle et qui étend aussi le langage CCS, et un nouveau calcul pour résoudre des problèmes d'optimisation distribués (par exemple des problèmes d'ordonnancement sur machine multi-coeurs) en utilisant une approche co-inductive.

Les membres de ce projet ont participé de manière active à l'émergence de ces paradigmes. Ce projet cible des problèmes théoriques qui ont une pertinence pratique.

Partenaires

INRIA INRIA Paris-Rocquencourt

Laboratoire public

PPS UNIVERSITE DE PARIS 7

Aide de l'ANR 426 055 euros
Début et durée janvier 2012 - 48 mois

 

Programme ANR : Blanc International II - SIMI 2 - Science informatique et applications (Blanc Inter II SIMI 2) 2011

Référence projet : ANR-11-IS02-0002

Coordinateur du projet :
Monsieur Gilles Dowek (INRIA Paris-Rocquencourt)
gilles.dowek@nullinria.fr

 

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.