LOGIQUE DE LA PROGRAMMATION
Présentation thématique
|
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 groupe
de travail avec des chercheurs du LIF.
Elle est impliquée dans plusieurs projets :
- ACI NIM « Géométrie du calcul » (GEOCAL) qui se termine en décembre 2006,
- Programmes blancs de l'ANR 2005 et 2006 : INVAL, PRELUDE,
MAREBIO, et SOAPDC,
- Responsable du groupe de travail « Géométrie du calcul » au sein du GDR
« Informatique mathématique ».
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 8 doctorants (dont deux soutiendront en décembre 2006).
L'équipe a organisé plusieurs rencontres internationales de haut niveau,
notamment la session résidentielle « Géométrie de calcul » de 5 semaines en
février 2006 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.