Les objectifs de recherche dans cette équipe sont d'analyser et développer les bases mathématiques et logiques pour la conception et l'implantation de langages de programmation et de leurs environnements.
L'outil fondant l'unité de ces recherches est le
-calcul et la théorie des types,
qui sont à la base des langages de programmation fonctionnels.
Les études dans ce domaine sont à la croisée des chemins
entre l'informatique,
l'algèbre (la théorie des catégories) et la logique mathématique.
La riche interaction entre ces trois pôles fait dans le monde
l'objet d'actives recherches, dont rendent compte les livres
[110, 109]. Deux autres livres-monographies,
publiés aussi par des membres de l'équipe, participent de ce
rayonnement [113, 111].
Une grande partie de l'intérêt du travail mené dans l'équipe provient du va-et-vient entre syntaxe, modèles et leurs applications aux langages de programmation. Des efforts particuliers portent sur l'intégration du paradigme de la programmation fonctionnelle avec d'autres paradigmes ou modèles de calcul, principalement la programmation orientée objet d'une part, les calculs de processus communiquants d'autre part.
Au chapitre de la communication, on peut souligner le succès remporté par la revue Mathematical Structures in Computer Science, Cambridge Univ. Press, dirigée par G. Longo, qui est devenue une revue de référence dans le domaine des fondations logiques et mathématiques de l'informatique. La préoccupation de diffusion de la connaissance est par ailleurs attestée dans l'équipe par l'importance des efforts d'enseignement dans les DEA et les écoles de printemps ou d'été, ainsi que par la participation à une vingtaine de Comités de Programme, depuis 1994.
La programmation orientée objet (OO) a connu un développement
considérable, sans jouir de bases aussi solides que celles qu'a pu
offrir le -calcul pour la programmation fonctionnelle. De
nombreux chercheurs s'intéressent à la formalisation dans un
cadre fonctionnel de différents concepts qui ont émergé dans
la communauté orientée-objet.
Les recherches de l'équipe se sont orientées dans deux
directions essentielles : surcharge et sous-typage.
On a d'abord étudié la ``surcharge'' comme ``dépendance fonctionnelle des types'', surtout grâce à la collaboration avec G. Ghelli (Pise). Les principales propriétés syntaxiques d'un calcul fonctionnel avec surcharge ont été données dans [127]. L'idée de base est qu'une des notions principales des systèmes à objets, le ``passage de message'', peut être traitée d'une façon fonctionnelle en considérant les méthodes comme fonctions globales et surchargées.
Les aspects théoriques tels que le second ordre [130], une surcharge pure [131] ou une interprétation formelle des langages à objets [129] on été étudiés de manière approfondie. Tous ces travaux ont permis de donner pour la première fois un fondement unique à différentes classes de langages a objets qui ont ainsi pu être intégrés dans un seul formalisme, comme montré dans le livre [111].
On ne s'est pas borné à considérer les aspects
théoriques.
En collaboration avec J. Boyland (Berkeley et Carnegie Mellon),
nous avons
démontré la faisabilité et l'importance pratique de ces
résultats. En
particulier, nous avons montré comment modifier le compilateur du
langages
O 
pour sécuriser le code généré [161] et comment
ajouter aux
langage Java les multi-méthodes [162] (un prototype
est disponible). Dans la même lignée nous avons défini en
collaboration avec
M.-V. Aponte (CNAM) une extension du système de modules de
SML [157].
Un élément important de l'interaction entre quantification du second ordre et sous-typage est la quantification bornée. Une formalisation de la quantification bornée avec sous-typage décidable a été développée avec B. Pierce (LFCS-Édimbourg), et a abouti à la définition du système décrit dans [165]. Le second ordre a été utilisé pour étudier la décidabilité des langages à délégation [182] en collaboration avec L. Liquori (Universitá di Torino). On a ensuite étudié l'extension de la quantification bornée par la surcharge et la liaison tardive. Le formalisme obtenu reprend les idées fondamentales du calcul en [127], mais le mécanisme de la surcharge est implanté par un polymorphisme de type explicite [130]. Ceci permet de résoudre les problèmes de perte d'information du calcul originaire, problèmes que l'on retrouve dans certains langages de programmation commerciaux. On a aussi entamé un approfondissement des possibilités d'application de l'approche de [127] aux bases de données [161], à une meilleure compréhension des rapports entre ``covariance'' et ``contravariance'' [128], aux méthodes binaires [123] et aux systèmes de modules [157].
Au-delà des modèles spécifiques, il n'y avait pas, jusqu'à présent, d'approche logique ou catégorique générale au sous-typage, dans un cadre fonctionnel. Une des activités principales en 1994 et 1996 a été la conception de la ``Logique pour le sous-typage'', développée avec K. Milsted (CNET, France Telecom) et S. Soloviev (St. Petersbourg) [183, 146]. Ce travail crée un nouveau lien entre paramétricité fonctionnelle (voir plus bas) et héritage. On a aussi suggéré une simplification intéressante du langage défini dans [127], ainsi que des nouvelles applications dans le cadre de la démonstration automatique. Un survol de quelques résultats récents est donné dans [150].
Notre équipe a participé dès l'origine à la définition et à l'implantation du langage CAML dont différentes versions ont été développées depuis, principalement à l'INRIA. Notre contribution concerne la compilation, le développement de bibliothèques et la diffusion du langage dans l'industrie et l'enseignement.
L'effort a surtout porté sur la réalisation d'un compilateur de ML vers C baptisé CEML. La compilation de ML vers C permet de produire, à partir de programmes fonctionnels, du code C portable et intégrable à des logiciels très divers.
Un point important à noter est que le compilateur réalisé permet en particulier une assez bonne lisibilité du code C produit, permettant ainsi d'utiliser des outils de mise au point de C comme par exemple des profileurs.
Par ailleurs, en collaboration avec l'Université de Montréal, une extension de ML au parallélisme de données a été réalisée [188, 179].
Différentes bibliothèques ont été réalisées pour étendre ou faciliter l'utilisation de ML. Le système MLGRAPH a été développé pour fournir une première couche de fonctions graphiques permettant la programmation en ML de dessins techniques complexes en utilisant toute la puissance du langage. Il combine la puissance du modèle graphique du langage POSTSCRIPT et la puissance d'expression de ML. Une de ses utilisations possibles est la programmation simple d'illustrations pour la documentation de systèmes, l'écriture de livres ou d'articles techniques pour laquelle la combinaison LaTeX-MLGRAPH s'avère particulièrement agréable. Dans cette optique une interface avec LaTeX a été réalisée [168]. Cet outil permet en particulier de construire des images CAML contenant du texte composé en LaTeX. L'ensemble de ces travaux est résumé dans [133].
Enfin, une extension de ML a été définie [318] pour permettre l'expression de contraintes sur les domaines finis, à la manière du langage CHIP. Cette extension, implantée comme une bibliothèque, permet de combiner dans le même programme une partie purement fonctionnelle et une partie de résolution de contraintes.
De notre point de vue, la programmation fonctionnelle est loin d'avoir atteint aujourd'hui le potentiel d'utilisateurs qui est le sien. Des efforts particuliers sont donc nécessaires vis-à-vis de l'industrie et de l'enseignement.
Dans le cadre d'une aide financée par le Ministère de la Recherche et de la Technologie, nous avons participé à une recherche contractuelle en collaboration avec Dassault-Aviation et l'INRIA et visant au développement de ``programmes temps-réel sûrs'' [210]. Ce projet visait à l'étude de faisabilité d'une ``chaîne de production'' de programmes prouvés corrects dans un contexte industriel utilisant le langage CAML comme langage intermédiaire entre un spécification écrite en Coq et un programme final écrit en C.
Par ailleurs, un ouvrage sur la programmation fonctionnelle et ses applications a été rédigé [201] (en anglais [202]).
Les liens entre -calcul (celui-ci pouvant être vu comme
un langage de programmation ou comme un langage de preuves
intuitionnistes) et la théorie des catégories ont sous-tendu une
grande partie de la recherche en sémantique depuis une bonne
dizaine d'années. Une spécificité du travail mené dans
l'équipe est de pousser loin l'exploitation syntaxique de ces
liens (substitutions explicites, isomorphismes de types et
réécriture), jusque dans l'étude des modèles (algorithmes
séquentiels et jeux).
La compilation catégorique du -calcul de P.-L. Curien
avait fourni un calcul de combinateurs catégoriques (1983) et une
machine abstraite, la CAM, qui avait servi à l'implantation du
langage CAML (1985). Depuis a été développé un
calcul plus proche du -calcul, appelé
-calcul, ou
calcul des substitutions explicites, qui fournit un cadre formel
pour étudier la gestion de la portée des variables dans
l'implantation des langages de programmation. On a mené
une étude fine des propriétés de terminaison des
substitutions [137]
et des propriétés de confluence du -calcul [136].
L'avancée la plus récente, en coopération avec Delia Kesner du
LRI d'Orsay, e été la mise en évidence d'un
rapport précis entre substitutions explicites et logique
linéaire, qui a permis d'obtenir une preuve de normalisation pour
des calculs de substitutions explicites typés par traduction dans
les réseaux de preuves [176]. Ce travail ouvre des
perspectives nouvelles, et permet d'envisager
la possibilité de trouver un calcul de substitutions explicites
avec toutes les bonnes propriétés, qui serait la réponse
adéquate au contre-exemple de Melliés (qui a montré la
non-terminaison du -calcul typé).
La sémantique catégorique des -calculs suggère une
question naturelle et d'utilité pratique : quels sont les
isomorphismes de types vérifiés dans tous les modèles ? Les
résultats obtenus sont rassemblés dans le livre
[113]. Ces travaux ont donné lieu à des
réalisations pour l'environnement du langage CAML LIGHT : un
programme de recherche en librairie a été diffusé avec le
système CamlLight 0.6, et une version très évoluée de ce
programme a été réalisée par deux élèves de l'ENS
(Vouillon et Jalon) pour CamlLight 0.7 .
Plus récemment, en coopération avec M.-V. Aponte du CNAM, cette approche a été généralisée aux modules de Objective-CAML [158]. Une implantation est en cours pour ce nouvel outil.
Le travail sur les isomorphismes de types a à son tour
motivé l'étude
de systèmes de réécriture confluents pour des
-calculs avec règles d'extensionnalité
[175, 177, 142, 178, 173]. Ces travaux,
menés en collaboration avec D. Kesner (Paris XI), et plus
récemment avec A. Piperno (La Sapienza, Rome), et N. Ghani
(Birmingham, UK, post doc au LIENS en 95 et 96) reposent sur une
interprétation expansive des règles d'extensionalité. Une
importante activité internationale s'est concentrée sur ce sujet
récemment.
La séquentialité s'occupe de la détermination des informations d'entrée nécessaires à la production d'une sortie donnée. Des progrès ont été accomplis dans plusieurs directions.
-calcul typé avec arithmétique et
récursion) étendu par des opérateurs de contrôle (semblables
aux constructions ``catch'' et ``throw'' de LISP). Ces travaux ont
été menés en collaboration avec R. Cartwright et M. Felleisen
(Rice, Houston) [126].
Les algorithmes séquentiels fournissent un modèle pour un
fragment important de la logique linéaire, et des correspondances
intéressantes ont été établies avec des sémantiques de
jeux développées complètement indépendamment [116]. -calcul, les langages
fonctionnels, la logique linéaire, etc... Des premiers résultats
ont été obtenus dans
ce sens [140]. P.-L. Curien organise sur ce sujet un groupe
de travail
intitulé ``Jeux et Chemins'', en liaison avec l'Équipe de Logique
de Paris VII. -calcul a été entreprise [184].
Le polymorphisme (ou pluralité des types) explicite, présent
dans des langages comme ceux de la famille ML, implique une
uniformité, ou paramétricité, de la dépendance des termes
par rapport aux types [119]. Une étude, en collaboration
avec M. Abadi et L. Cardelli (Digital-SRC, Palo-Alto), a conduit à
un système de raisonnement relationnel appelé 
assez
puissant pour montrer formellement des propriétés de programmes
qui sont établies à partir de leur type seulement,
et non de leur code. Un modèle du système a
été construit [159].
Sur un autre thème, relié á la paramétricité par le
travail précédent de Longo (en collaboration avec S. Soloviev et
K. Milsted), on a obtenu des résultats qui justifient les
définitions imprédicatives en théorie des types, grâce à
une notion originale (les "preuves prototypes", voir [180])
et des résultats de cohérence et décidabilité.
-calcul et parallélisme
L'intégration d'une dose de
non-déterminisme dans le modèle
fonctionnel a, du point de vue théorique, au moins deux
origines : la première remonte aux années
70 et concerne l'étude des fonctions multivaluées et de la
complétude
des modèles à la Scott
du -calcul ;
la deuxième correspond aux codages de diverses stratégies du
-calcul dans des calculs de processus, qui soulignent les
différences entre les modèles fonctionnel et distribué.
L'introduction de la notion de ressource dans le lambda-calcul par
Boudol en 93 trouve là
sa motivation.
On s'est intéressé
à l'étude des fonctionnalités propres aux
calculs de processus dans le cadre du -calcul,
en particulier le -calcul avec ressources
qui combine non-déterminisme et blocage [195].
Le travail a suivi deux axes
principaux : expressivité et sémantique.
La question de l'expressivité est en gros de savoir si un langage peut
être utilisé à la place d'un autre sans modifier la notion
d'équivalence. Des sémantiques
(dénotationnelle [195] et algébrique par
approximants [181]) ont été définies
pour le calcul avec ressources.
Tout le cadre
théorique propre au -calcul a été considérablement
modifié : équation aux domaines, fonction
d'interprétation, notion d'approximant. Des résultats
d'adéquation ont été montrés pour les modèles de filtres
associés aux équations aux domaines ; en revanche, pour obtenir
la complétude, il a été nécessaire d'introduire un test de
convergence séquentiel
[160, 208].
Des intérêts en Logique, Épistémologie et ``Théorie de la connaissance'' sont présents dans l'équipe. Ils ont trouvé des débouchés intéressants à Paris grâce aux activités du groupe interdisciplinaire ``Cognition'' de l'ENS, coordonné par G. Longo, qui ont permis l'organisation d'un séminaire régulier et de plusieurs colloques à l'ENS (voir Diffusion). Ces activités sont aussi à l'origine des invitations à des colloques (voir Séjours, conférences et séminaires) et à la rédaction de [218, 120, 155, 156, 219, 121], ainsi que des compte-rendus [214, 217, 220]. Le projet à la base de ces activités est en train de se préciser et vise à une réflexion sur les rapports entre fondements logiques et fondements ``cognitifs'' des mathématiques (voir en particulier [155, 220]).
On trouvera ci-dessous quelques directions non encore mentionnées dans lesquelles des résultats sont espérés dans les années qui viennent.