Preuves, Programmes et Systèmes

Présentation du laboratoire PPS

PPS est un laboratoire qui fédère les énergies de chercheurs, enseignants-chercheurs et doctorants issus de cultures différentes (informatique et logique mathématique) pour travailler sur une thématique assez précise : celle des langages de programmation et des systèmes distribués, et de leurs fondements logiques. Notre projet de recherche est en effet fondé sur la conviction que la logique (et plus particulièrement la théorie de la démonstration), mais aussi la théorie des catégories, et d'autres théories mathématiques comme l'homologie ou l'homotopie, ou les probabilités, ont une part importante à jouer pour élucider le sens des programmes, afin de les rendre plus sûrs, et qu'inversement l'informatique, comme la physique a pu l'être et continue de l'être, peut être une source dans laquelle la logique et d'autres domaines des mathématiques peuvent puiser pour se renouveler.

Une grande part de la recherche théorique menée à PPS reste inspirée par la correspondance de Curry-Howard : c'est une découverte des années 1960 qui semblait n'avoir qu'une portée mineure, mais qui s'est révélée d'une importance capitale. Elle établit en effet une relation tout-à-fait remarquable entre les preuves et les programmes, qui transforme le λ-calcul en un puissant outil de théorie de la démonstration : les intuitions informatiques deviennent fondamentales en logique mathématique. Et il est fascinant de constater qu'il y a une réciproque : les méthodes de logique deviennent essentielles pour des problèmes importants posés par l'industrie informatique. Le tout premier étant le problème de la correction des programmes. Un vérificateur de preuves comme CoQ, développé à l'INRIA sur la base d'une extension de la théorie des types de Martin-Löf (le «calcul des constructions»), et qui est donc fondé sur la correspondance de Curry-Howard intuitionniste, est effectivement utilisé dans l'industrie pour prouver des programmes.

La correspondance de Curry-Howard s'applique dans plusieurs contextes : au départ à la logique intuitionniste (qui n'accepte par le tiers exclu), puis à la logique linéaire, qui réconcilie le caractère constructif de la logique intuitionniste (lequel garantit, par exemple, que toute preuve d'existence peut fournir un témoin) avec les symétries de la logique classique, et enfin à la logique classique.

Il s'agit donc d'un domaine du plus haut intérêt, entre logique et informatique, qui renouvelle complètement nos idées sur les démonstrations mathématiques, et qui est riche d'applications, non seulement à la preuve de programmes, mais aussi à la théorie des langages de programmation, au parallélisme, à la communication, etc.

Les thématiques du laboratoire peuvent être regroupées en six directions principales :

Jeux et modèles de la programmation.

La distinction traditionnelle entre syntaxe et sémantique s'est bien atténuée, faisant apparaître certains modèles comme de la syntaxe épurée. Comme le titre l'indique, il y est beaucoup question de modèles de jeux, devenus l'objet d'actives recherches depuis une dizaine d'années, et de polarités, apparues plus récemment.

Théorie de la démonstration et λ-calcul.

Dans ce thème, intimement lié au précédent, l'accent est mis sur la syntaxe : notamment élimination des coupures (la contre-partie logique de l'évaluation des programmes) et réseaux de preuves (qui sont des représentations géométriques des preuves que la logique linéaire a permis de construire), mais aussi dualités de calcul, et bon vieux λ-calcul (la charpente syntaxique de la logique intuitionniste et des langages de programmation fonctionnelle) simplement typé. Avec la création de l'Équipe Projet Commune πr² (INRIA Rocquencourt - PPS), le laboratoire est devenu le principal maître d'oeuvre du développement du noyau du système d'aide à la preuve Coq. Il participe activement à la recherche théorique sur le calcul des constructions (formalisme à la base de Coq) et sur ses extensions.

Spécifications et réalisabilité.

L'ambition ici est de débusquer quel programme se cache derrière tel ou tel théorème des mathématiques. Il fallait commencer par la logique classique, puis prendre les axiomes de la théorie des ensembles. Le principal outil pour cette étude est la réalisabilité, qui prend un peu le contre-pied des deux thèmes précédents en ce qu'elle ne suppose pas les formules avant les preuves, mais au contraire considère les formules comme des spécifications, ou ensembles de programmes (non typés) ayant le même comportement.

Réécriture.

Ici, l'on déborde du strict cadre de la logique pour étudier les propriétés des systèmes de réécriture et des systèmes de réécriture d'ordre supérieur (c'est-à-dire avec variables liées), pour lesquels le cadre des calculs de substitutions explicites est très utile. Un bon laboratoire d'utilisation des techniques de réécriture est celui des isomorphismes de types (avec des applications informatiques à la recherche de programmes en bibliothèque). Des méthodes axiomatiques pour la réécriture ont été développées. Un autre thème encore en émergence est celui de la réécriture n-dimensionnelle, où il ne s'agit plus de réécrire des mots ou des termes, mais aussi des surfaces, des volumes, etc.

Programmation.

Le laboratoire développe de nouvelles méthodes dans des domaines qui vont des protocoles réseau jusqu'aux applications Web en passant par des nouvelles approches du génie logiciel. Ces développements mettent en oeuvre des outils formels et rigoureux basés sur la théorie des types et la logique. Cette activité s'est renforcée avec la création de l'Initiative de Recherche et Innovation sur le Logiciel Libre (IRILL), structure d'accueil commune à l'INRIA, l'Université Paris Diderot et l'UPMC.

Logique, Concurrence et Modélisation.

Un nouveau front de recherche s'est ouvert à PPS, autour de la modélisation de la programmation dite concurrente (calculs de processus) et mobile, qu'il s'agisse d'en rechercher les fondements logiques (nous avons une certaine expérience dans ce domaine), ou de les appliquer à une troisième science : la biologie, et plus précisément à la modélisation des processus de la biologie moléculaire.

Pour une présentation plus détaillée du laboratoire, vous pouvez consulter les Rapport de Recherche PPS (2003, 2007).