Cette page n'est plus à jour!

L'équipe LDP, fondée par Jean-Yves Girard en 1992, fait porter sa recherche sur la logique mathématique, la théorie de la démonstration et la théorie du calcul, ainsi que sur les interactions entre ces théories et d'autres disciplines, notamment les mathématiques, l'informatique, la linguistique, la philosophie et la biologie.

Collaborations, projets, animation scientifique

L'équipe a de nombreuses collaborations avec des laboratoires en France (Marseille, Paris, Montpellier, Sophia-Antipolis, Grenoble, Chambéry, Nancy) et à l'étranger (Italie, Royaume-Uni, Allemagne, Canada, Etats-Unis, Japon). Au niveau local elle participe aux activités de la FRUMAM, et organise un séminaire de logique. Elle est impliquée dans plusieurs projets :

L'équipe a fait passer 6 thèses sur la période 2000-2006, qui ont toutes débouché sur un recrutement au CNRS ou à l'Université ; elle compte à l'heure actuelle 7 doctorants. L'équipe a organisé plusieurs rencontres internationales de haut niveau, notamment la session résidentielle « Logique et interactions » de 5 semaines en février 2012 au CIRM qui comprenait une école d'hiver et plusieurs ateliers thématiques et a rassemblé plusieurs centaine de chercheurs.

Recherche

Sur le plan scientifique l'équipe s'est récemment ouverte à de nouveaux champs d'application: théorie homotopique du calcul, combinatoire des relations, vérification automatique, logique et philosophie, systèmes discrets et biologie. Le paradigme initial est la correspondance de Curry-Howard, qui relie preuves et formules logiques aux concepts informatiques de programmes (termes du lambda-calcul) et types. Ce paradigme est à l'origine d'un grand nombre de développements (notamment la logique linéaire de Girard), sujets de recherche pour plusieurs membres de LDP.

Lambda-calcul et logique linéaire

Girard a récemment poussé plus loin son analyse de l'élimination des coupures en terme de géométrie de l'interaction, dans laquelle l'élimination des coupures s'exprime comme la résolution d'une équation du feedback qui peut se résoudre de façon très générale dans un cadre d'algèbres d'opérateurs. Dans une direction similaire, Cosentino poursuit sa thèse sur le lien entre logique et physique quantique, en essayant d'appliquer la géométrie de l'interaction généralisée de Girard.

La correspondance de Curry-Howard comporte d'autre part un volet "sémantique dénotationnelle". De telles sémantiques de la logique linéaire dans les espaces de Köthe et les espaces de finitude sont à l'origine du lambda-calcul différentiel (Regnier, Ehrhard, Vaux, De Falco), qui sur le plan mathématique introduit en logique des constructions inspirées du calcul différentiel (développement de Taylor), qui peuvent également s'interpréter informatiquement comme une extensions du lambda-calcul avec ressources de Boudol. 
Une classe de réseaux d'interaction (extension due à Lafont du cadre des réseaux de preuve de la logique linéaire) a été proposée pour ce calcul : les réseaux différentiels. Mazza travaille également sur les réseaux d'interaction, plus spécifiquement sur leur sémantique et leurs extensions concurrentes.

Partant d'une proposition de Métayer d'interpréter les réseaux de preuve comme des surfaces compactes orientées, Andreoli, Pulcini et Ruet ont proposé un plongement naturel de la logique linéaire et du calcul de Lambek dans la logique permutative. 
Autre thématique qui s'est développée récemment: le lien entre la logique, et plus précisément la ludique de Girard, et la linguistique (Fleury, Quatrini). La ludique est également le domaine de la thèse de Duchesne.

Théorie homotopique du calcul

Lafont travaille avec Métayer sur la notion clef de résolution polygraphique de Métayer, qui s'exprime elle-même en termes de polygraphes de Burroni ou de computades de Street. Cette notion devrait permettre d'unifier et de généraliser des approches qui sont visiblement apparentées comme les théorèmes de cohérence en théorie des catégories (Mac Lane...), les invariants homologiques et homotopiques de la réécriture (Squier...) ou l'homologie des groupes Gaussiens (Dehornoy, Lafont). Dans cet esprit, ils ont dressé une liste d'une quinzaine de conjectures ou de directions de recherche (programme de Minneapolis).

Combinatoire des graphes et des relations

C'est principalement le domaine de recherche d'Ille, qui s'intéresse principalement à la décomposabilité, pour la somme lexicographique, des structures combinatoires. En généralisant l'arbre de décomposition au cas infini, il a notamment résolu la conjecture de Sabidussi (1960) sur les graphes idempotents pour le produit lexicographique. D'autres travaux ont été menés en théorie des ordres : dénombrement des réalisateurs, reconstruction et monomorphie. Enfin, avec Ruet, il a résolu un problème de complexité algorithmique sur les variétés d'ordre, structures combinatoires qui jouent un rôle fondamental dans la logique non-commutative d'Abrusci et Ruet.

Algorithmique pour la sûreté du fonctionnement

A. Rauzy et Minh-Thang travaillent sur l'évaluation du risque et de ses conséquences du risque dans des installations industrielles sensibles : centrales nucléaires, industries chimiques et pétrolières, avionique, transports... Pour cela, les ingénieurs font des modèles et emploient donc des formalismes de description, principalement des formalismes Booléens ou des formalismes états/ transitions (automates d'états finis, réseaux de Petri...). Une fois l'installation décrite par un modèle, il faut se servir de ce modèle pour évaluer les quantités (en général probabilistes) qui mesurent du risque et ses conséquences, et les problèmes qui en découlent sont en général NP-difficiles ou #P-difficiles.

Logique et philosophie

Sous la direction conjointe de Girard et Livet, le travail de Tronçon porte sur la philosophie de la logique et vise à présenter une analyse contemporaine de la théorie de la démonstration et de ses rapports avec la cognition, l'informatique et la signification. Ils ont largement contribué à l'animation du groupe de travail "Logique et Interaction : vers une Géométrie de la Cognition".

Systèmes discrets et biologie

Les réseaux de régulation génétique sont à la base de toutes les fonctions biologiques. Leur complexité nécessite un travail de modélisation et des théorèmes reliant la structure de ces réseaux à leur dynamique. Ruet s'est particulièrement intéressé à des modèles discrets, voire Booléens. Il travaille d'une part avec Chaouiya, Remy et Thieffry sur des modèles reposant sur les réseaux de Petri (modèles de programmation concurrente), et d'autre part avec Remy, Thieffry et Crumière sur la formalisation et la preuve de "règles de Thomas" prédisant la structure à partir de certaines propriétés dynamiques.