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

Translate this page in english

Blanc - SIMI 2 - Science informatique et applications (Blanc SIMI 2) 2011
Projet RECRE

Réalisabilité pour la logique classique, la concurrence, les références et la réécriture

Le but de ce projet est d'acquérir une meilleure compréhension de la correspondance preuves/programmes pour la logique classique, à la lumière des avancées récentes issues de la théorie de la réalisabilité classique.

Aujourd'hui, cette correspondance est très développée et bien comprise dans le cas de la programmation fonctionnelle pure, sans effets de bord ni contrôle. Elle a des retombées remarquables à la fois sur le plan théorique et sur le plan pratique: ses apports concernent tant les modèles mathématiques de la logique intuitionniste et des mathématiques constructives que le développement des assistants à la preuve et des prouveurs automatiques, ainsi que la formalisation sur machine de résultats significatifs. Elle a permis d'utiliser des modèles mathématiques du calcul purement fonctionnel pour spécifier et certifier des programmes, notamment grâce à la technique de l'extraction de programmes à partir de preuves mathématiques.

À la suite de la découverte par Griffin, en 1990, d'une correspondance entre la logique classique et les opérateurs de contrôle, Krivine a développé une théorie de la réalisabilité classique, qui est une reformulation complète des principes de la réalisabilité dans le contexte du raisonnement classique. Au centre de cette théorie se trouve l'idée selon laquelle les réalisateurs d'une formule sont les programmes qui satisfont une certaine spécification associée à cette formule, cette spécifications étant formulée en termes d'interaction entre un programme et son environnement. De manière surprenante, cette construction peut être vue comme une généralisation de la notion de forcing introduite par Cohen dans les années 1960 en théorie des modèles, afin d'établir des résultats d'indépendance en théorie des ensembles, tels que l'indépendance de l'hypothèse du continu. La théorie de la réalisabilité classique a ainsi permis de donner récemment un contenu calculatoire à de tels axiomes à l'aide de traits de programmation très concrets, tels qu'une horloge globale et des primitives de gestion de la mémoire. Ces analogies remarquables suggèrent naturellement de nouvelles directions pour étendre la correspondance preuves/programmes au-delà du scope de la programmation fonctionnelle.

Le but de notre projet est de développer cette interprétation calculatoire de la logique et la technologie de la réalisabilité classique elle-même, en utilisant les domaines d'expertise de chercheurs dans des domaines voisins. En effet, la correspondance preuves/programmes est intrinsèquement interdisciplinaire car les domaines qu'elle touche vont de la logique mathématique à la conception des langages de programmation en passant par la théorie des catégories et l'informatique théorique. Nous nous proposons d'étudier les liens entre la réalisabilité, le forcing et les effets de bord (Tâche 2) ainsi que les applications possibles de cette technologie à l'extraction de programmes (Tâche 3). Nous nous proposons également de développer et de systématiser les techniques de réalisabilité dans le domaine de la programmation concurrente et des langages de bas niveau (Tâche 4), tout en étudiant les structures algébriques sous-jacentes à la réalisabilité à l'aide de la théorie des catégories et de la sémantique des jeux (Tâche 5).

Partenaires

CNRS DR 12 _ IML CNRS - DELEGATION REGIONALE PROVENCE CORSE

LIP ECOLE NORMALE SUPERIEURE DE LYON

PPS - pi.r2 INRIA Paris-Rocquerncourt

LAMA UNIVERSITE DE SAVOIE - CHAMBERY

Aide de l'ANR 631 280 euros
Début et durée du projet scientifique novembre 2011 - 48 mois

 

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

Référence projet : ANR-11-BS02-0010

Coordinateur du projet :
Monsieur Colin Riba (ECOLE NORMALE SUPERIEURE DE LYON)
colin.riba@nullens-lyon.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.