Blanc Inter II SIMI 2 - Blanc International II - SIMI 2 - Science informatique et applications

Approche Logique de Nouveaux Paradigmes de Calcul – Locali

Résumé de soumission

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.

Coordination du projet

Gilles Dowek (INRIA Paris-Rocquencourt) – gilles.dowek@inria.fr

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.

Partenaire

INRIA INRIA Paris-Rocquencourt
PPS UNIVERSITE DE PARIS 7

Aide de l'ANR 426 055 euros
Début et durée du projet scientifique : décembre 2011 - 48 Mois

Liens utiles

Explorez notre base de projets financés

 

 

L’ANR met à disposition ses jeux de données sur les projets, cliquez ici pour en savoir plus.

Inscrivez-vous à notre newsletter
pour recevoir nos actualités
S'inscrire à notre newsletter