Projet ANR Récré

Realizability for classical logic, concurrency, references and rewriting

Présentation

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 bien comprise dans le cas de la programmation fonctionnelle pure, sans effets de bord ni contrôle. Elle a des retombées remarquables sur le plan théorique comme 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.

Suite à 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 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 afin d'établir des résultats d'indépendance en théorie des ensembles (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 ainsi que les applications possibles de cette technologie à l'extraction de programmes. 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, 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.


On trouvera ici une description plus complète du projet en anglais

Rencontres

Les membres et sympathisants du projet Récré se recontrent à un rythme mensuel, notamment au sein du séminaire Chocola organisé à l'ENS de Lyon.