Projet ANR-11-BS02-0010 – RECRE : Réalisabilité pour la logique classique, la concurrence, les références et la réécriture
Programme : Blanc - SIMI 2 - Science informatique et applications (Blanc SIMI 2) 2011
Année de financement : 2011
Coordinateur du projet : Monsieur Colin Riba (ECOLE NORMALE SUPERIEURE DE LYON)
Partenaires : Institut de Mathématiques de Marseille; Laboratoire d'Informatique du Parallélisme; Conception, Étude et Implémentation de Langages pour les Preuves et les Programmes; Laboratoire de Mathématiques
Montant : 631280.0 euros
Date de début : 2011
Durée : 48 mois
Résumé : 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).