Logique et géometrie de l'interaction – LOGOI

L'hypothèse de travail qui sous-tend notre projet est que la théorie de la démonstration et l'informatique peuvent trouver de nouveaux fondements mathématiques empruntant à divers champs mathématiques : de l'analyse et la géométrie à la théorie de la mesure qui ont été des sujets d'intense développements des mathématiques contemporaines, à tel point que le point du vue sur ces domaines a radicalement changé. Les développements récents en géométrie de l'interaction ont rendu cela possible et nous ont servi de base de travail.
Nous espérions/escomptions tout particulièrement de nouveaux apports en théorie de la complexité. Les nombreuses approches de la complexité calculatoire existantes manquent fondamentalement de structure : la théorie de la complexité est jusqu'ici restée essentiellement une collection de techniques ad hoc chacune utile pour un type de problèmes particulier mais sans intérêt pour d'autres questions. La quasi-totalité des caractérisations disponibles sont de nature existentielle (l'appartenance à une certaine classe est caractérisée par l'existence d'un algorithme ou d'une machine tel que…) et non pas universelle.
Un autre objectif majeur de nos recherches consistait à ouvrir la voie à une théorie de l'expressivité des langages de programmation où l'on s'intéresse non pas à ce qui est calculé mais à comment le calcul est effectué.

Toutes ces lignes ont le potentiel de conduire à des applications intéressantes.

Nos travaux ont conduit à renouveler la syntaxe des preuves et à des avancées dans le fondement d'une théorie de l'interaction. L'un des résultats principaux est l'émergence d'une approche radicalement nouvelle de la complexité où les outils et méthodes viennet de la géométrie de l'interaction et de son interprétation dans les algèbres d'opérateurs. Nous avons ainsi gagné de nouvelles intuitions sur l'expressivité des langages de programmation et des modèles calculatoire.
Nos applications concernent notamment des champs de recherches très actif, comme le calcul quantique, la concurrence ou le calcul parallèle.

Parmi les succès de LOGOI, nous soulignons particulièrement :
implication élevée d'étudiants : le projet a directement impliqué 20 doctorants et plusieurs stagiaires de M2. Neuf thèses réalisées dans le cadre du projet ont déjà été soutenues.
dissémination et visibilité: deux écoles et plusieurs workshops ont été organisés.
réseau de collaboration internationales riche et dynamique.

`Les avancées importantes obtenues dans toutes les tâches du projet constituent les bases d'une approche vraiment nouvelle. En outre, un réseau de chercheurs s'est consolidé autour de cette approche, autour duquel nous avons la ferme intention de construire de nouveaux projets. '

Publications (référées ): 44 , dont 25% multi-paretenaires

Revues Internationales: 15
Actes de conférences internationales: 28
Actes de conférences nationales: 1

Thèses de doctorat : 9

Le projet LOGOI se situe à l’interface de la logique mathématique et de l’informatique théorique ; plus précisément en Théorie de la
Démonstration, branche de la Logique Mathématique qui s'occupe des propriétés des langages, mathématiques ou informatiques. C'est donc un cadre on ne peut plus naturel pour l'étude des langages de programmation.
L’évolution de la théorie du calcul et de la programmation (coopération entre agents, échange de données, ressources partagées, calcul quantique ...) demande un renouvellement fondamental de la Théorie de la Démonstration ; il faut, en effet, élaborer les concepts permettant de répondre aux nouveaux défis. 
La Théorie de la Démonstration propose et oppose, traditionnellement, deux paradigmes de calcul basé sur les démonstrations : 
- D'une part, les Preuves comme Programmes (popularisé sous le nom d'isomorphisme de Curry Howard), où l'on calcule par explicitation (normalisation, élimination des coupures) d'une démonstration donnée à l'avance. 
- D'autre part, les Preuves comme Recherche (popularisé par la programmation logique et le langage PROLOG), où l'on calcule en cherchant à démontrer une formule donnée à l'avance. 
La Logique Linéaire, en autonomisant la dynamique logique (i.e., les calculs sous-jacents) permet de réconcilier ces deux paradigmes --- pourtant réputés incompatibles et antagonistes --- sur la base d'une approche interactive qui englobe démonstrations, programmes et instructions de contrôle dans une même catégorie de processus.
Cette unification se fait en Géométrie de l'Interaction (et aussi en Ludique, paradigme voisin issu de la même Logique Linéaire). Comme le suggère le nom, les processus (= preuves, programmes, contraintes) sont définis relativement à leur comportement vis à vis de l’ interaction. Ce cadre conceptuel nous semble ainsi particulièrement propice à l'analyse de la procéduralité du calcul : il devrait amener des réponses appropriées aux défis actuels représentés par la complexité algorithmique, le calcul quantique et la théorie de la concurrence.
Au niveau logique proprement dit, l’approche dynamique de la Géométrie de l’Interaction, si elle rend bien compte de la procéduralité et du temps de l’exécution des programmes, concerne également la notion de vérité, qui perd son caractère absolu, primitif (et pléonasmatique), pour prendre une valeur interactive, contextuelle... En accord de principe avec la "philosophie" de la mécanique quantique, un accord de principe renforcé par l'utilisation des algèbres de von Neumann (le facteur hyperfini dans la plus récente version de la Géométrie de l'Interaction).
Nous espérons trouver dans les algèbres d'opérateurs le cadre approprié permettant de dépasser les limitations théoriques du langage usuel (trop circonscrit au monde combinatoire) pour comprendre le "moteur" qui anime la complexité algorithmique, i.e., la différence entre question et réponse, trouvaille et vérification. Techniquement, cela veut dire mener à maturité l'étude des concepts novateurs introduits en Logique Linéaire : typiquement, les exponentielles allégées emblématiques de ce nouveau regard logique sur la complexité algorithmique, sans oublier les autres artefacts novateurs de la Logique Linéaire, réseaux de démonstrations ou Ludique, qui sont plus que jamais d'actualité.