Pierre-Louis Curien

Recevez la lettre d'information

Télécharger la lettre d'information

Pierre-Louis Curien ou la passion sémantique


Informaticien théoricien, directeur de recherche CNRS émérite à l'IRIF et membre de l´équipe-projet Pir2 (Inria/Université de Paris/CNRS), Pierre-Louis Curien voit cette année sa carrière couronnée par le Grand Prix Inria – Académie des sciences. Pour la FSMP, il a accepté de se confier sur son parcours, marqué par d’heureuses rencontres, et sur ses travaux dans lesquels il explore les territoires les plus abstraits de l’informatique, là où affleurent les mathématiques, nous offrant une petite incursion dans le monde passionnant de la sémantique des langages de programmation, ou nous entretenant des liens entre informatique fondamentale et théorie de la preuve mathématique.

Question : Êtes-vous devenu scientifique par tradition familiale ?
Pierre-Louis Curien : Mon père était physicien, un de mes frères, économiste, est polytechnicien donc oui, je suppose que l’on peut parler de tradition familiale, même s’il n’y avait pas de pression explicite pour que je fasse des sciences. J’ai surtout eu le privilège d’habiter le quartier latin et d’être scolarisé dans les excellents lycées Henri IV et Louis-le-Grand. Là, j’ai eu notamment deux professeurs de mathématiques absolument géniaux. D’abord mon enseignante de seconde, Elisabeth Dognin, qui m’avait donné un problème de concours général qui m’avait pas mal occupé. Et puis, en première et en terminale, Denis Gerll, qui a d’ailleurs formé plusieurs mathématiciens reconnus, et qui offrait aussi aux élèves qu’il détectait comme, disons, les plus agiles, des questions à chercher un peu hors des sentiers battus.

Q : Vous avez donc su très tôt quelle carrière vous vouliez faire ?
PLC : Pas tout à fait. Après avoir intégré l’ENS, j’ai eu des doutes. Je m’intéressais aussi beaucoup aux langues. Il se trouve que mon grand-père maternel, Georges Dumézil, était un grand spécialiste des langues indo-européennes, qui maîtrisait une trentaine de langues et avait même sauvé de l'oubli une langue du Caucase, l’oubykh, dont il avait recueilli les sons et l’héritage culturel auprès de son dernier locuteur afin d'en établir la grammaire et le dictionnaire avant son extinction. J’ai discuté avec un linguiste de l’université Paris 7, Maurice Gross. Je lui ai expliqué : je suis agrégé de maths mais je m’intéresse aux langues, qu’est-ce que je fais ? Il m’a suggéré de m’intéresser aux langages de programmation. C’est ainsi que j’ai fait le DEA d’informatique fondamentale de Paris 7 : c’était à la fois très mathématique, car c’est de l’informatique très théorique, et en même temps, ce n’était pas sans lien avec la notion de langage, de langue.

Q : Êtes-vous resté un linguiste amateur ?
PLC : J’aime capter les sons des langues des pays que je visite mais je ne parle « que » le français, l’anglais, l’italien, l’allemand et le chinois, ce qui, par rapport aux linguistes, est infime.

Q : Quel est le moment déterminant de votre carrière ?
PLC : Je dirais que c’est le choix de mon lieu et de mon sujet de thèse. Après mon DEA, sur la théorie des automates, je cherchais une bourse de doctorat. Gérard Berry, alors jeune chercheur, avait un financement et cherchait un thésard. Le poste était basé à Sophia Antipolis et comme je faisais du deltaplane à cette époque, j’ai dit : génial ! Le sujet, la sémantique des langages de programmation, était très éloigné de ce que j’avais fait en DEA. Il s’agissait de comprendre le sens qu’ont des bouts de code. Je me suis notamment mis à travailler sur le lambda-calcul.

Q : Pouvez-vous nous expliquer ce qu’est le lambda-calcul ?
PLC : C’est un langage extrêmement simple, très épuré, mais extrêmement puissant, et dont la théorie est très compliquée. Ce langage a été le premier support pour expliquer la notion de fonctions calculables. Inventé par Alonzo Church deux ans avant la machine de Turing, le lambda-calcul est lié à la théorie de la calculabilité. Les familles de langages qui s’inspirent du lambda-calcul sont des langages dits fonctionnels, par opposition aux langages impératifs. Dans la programmation fonctionnelle, on ne parle pas d’instructions mais de fonctions, on est censé écrire des fonctions, comme Fibonacci ou la factorielle. Dans la syntaxe du lambda-calcul, « lambda x quelque chose » est la fonction qui à x associe quelque chose, par exemple, si ce quelque chose est « 4 + x », cela donne la fonction qui prend un entier et qui rend « 4 + cet entier ». Le lambda-calcul est le squelette d’autres langages, c’est en particulier la partie fonctionnelle du langage OCaml créé à Inria et utilisé par les milieux de recherche pour certifier d’autres recherches.

Q : Où se situe votre contribution dans ce domaine ?
PLC : Comme je l’ai dit, mes travaux portaient sur la sémantique des langages de programmation. En théorie du langage, la syntaxe, c’est le langage lui-même, tandis que la sémantique, c’est quel sens on donne aux termes de ce langage. Il y a plusieurs façons de voir les choses. On peut dire que le sens de ces termes, c’est comment ils s’exécutent. Par exemple, le sens de l’addition c’est « 4 + 5 = 9 ». Mais on peut aussi définir l’addition de manière plus abstraite, par récurrence. La sémantique consiste donc soit à expliciter comment les langages s’exécutent (on parle de sémantique opérationnelle), soit à utiliser les mathématiques pour donner un sens aux programmes en tant que fonctions dans certains espaces mathématiques, par exemple, l’ensemble des fonctions des entiers dans les entiers. On a les langages d’un côté et leurs interprétations dans un espace mathématique de l’autre. Fournir un modèle d’un programme, c’est donner un sens à ce programme dans un certain espace mathématique. Il existe des programmes qui ne se terminent jamais mais qui fournissent toujours plus d’information : par exemple, un programme qui calcule la liste les nombres premiers. On voit bien que pour modéliser ce programme, on a besoin de notions mathématiques comme la notion de limite. Plus généralement, on a besoin de mathématiques pour interpréter les programmes. C’est ça, la sémantique des langages de programmation, ou sémantique dénotationnelle.

Q : Comment a évolué ce sujet de recherche ?
PLC : Le sujet de la sémantique des langages de programmation date de la fin des années 1960. Je fais partie de la seconde génération de personnes à avoir travaillé dessus. Quand j’ai commencé à m’intéresser aux modèles du lambda-calcul, il s’agissait d’interpréter les programmes sur des ensembles ordonnés complets, c’est-à-dire pourvus d’une notion de limite. Plus récemment (à la fin des année 2000), le sujet a connu une révolution grâce à Vladimir Voevodsky (médaille Fields 2002), qui leur a donné du sens sur des espaces topologiques à déformation près, appliquant la théorie de l’homotopie aux programmes. Il ne s’agissait pas seulement de donner un sens à un programme, de dire « tel bout de code calcule telle fonction qu’on pourrait exprimer différemment du programme », mais aussi de pouvoir dire si tel programme fait la même chose que tel autre programme (par exemple, si on veut optimiser un programme, il faut pouvoir s’assurer que le programme modifié fait vraiment la même chose que le programme initial). Avec cette vision des choses, on peut considérer un programme « à équivalence près ». Autrement dit, un programme se déforme en un autre programme comme un espace topologique se déforme en un autre espace topologique.



Q : Vous avez apporté votre contribution au langage OCaml.
PLC : Pour le langage OCaml, j’ai donné un modèle d’exécution c’est-à-dire une machine abstraite (le « Cam » de OCaml signifie « categorical abstract machine »), une traduction de ce langage dans un langage plus exécutable. Moi qui ne suis pas un programmeur, je suis arrivé là de manière très abstraite. J’ai été obligé de travailler dans une branche des mathématiques qui s’appelle la théorie des catégories. J’ai interprété le langage du lambda-calcul dans la théorie des catégories et j’ai réalisé que la théorie des catégories était un langage de programmation. On peut dire que j’ai pris une abstraction mathématique et que j’ai réussi à en faire un langage machine, ou du moins un langage intermédiaire. Faire un langage et l’implémenter, c’est un travail d’équipe. Le chef d’orchestre de cette équipe, c’était Gérard Huet (qui a d’ailleurs reçu ce même Grand Prix Inria-Académie des Sciences en 2011). C’était lui l’architecte du langage Caml au début. Puis est arrivé un autre personnage, Xavier Leroy (Grand Prix Inria-Académie des Sciences en 2018, aujourd’hui titulaire de la chaire d’informatique du Collège de France). C’est lui, le grand héros de OCaml. Xavier Leroy est un vrai programmeur, et en même temps quelqu’un qui aime la théorie. Il maîtrise tout le spectre de l’informatique, contrairement à moi qui me situe au niveau le plus abstrait et qui tend vers les mathématiques. C’est lui qui a mis au point l’implémentation de OCaml.

Q : Vos travaux touchent aussi à la logique, au lien entre preuve mathématique et programme.
PLC : Quand j’ai travaillé sur le lambda-calcul, j’y ai travaillé sans me rendre compte que je faisais de la logique – d’ailleurs, au tout début, je n’en faisais pas, en réalité. Mais il existe une correspondance très profonde entre programmes et preuves (on nomme correspondance de Curry-Howard le pont entre informatique théorique et théorie de la démonstration). Une preuve mathématique, quand elle est complètement écrite, c’est un programme. Donc tout ce travail pour comprendre ce qu’est programme, se retranscrit en compréhension de ce qu’est une preuve mathématique. La théorie des types permet également d’exprimer cette correspondance : un programme a un type, et un type correspond à une formule. J’étais l’un des organisateurs d’un trimestre Preuves et programmes consacré à ces questions, en 2014 à l’IHP (au sujet de ce trimestre, voir ici le hors-série de MathsInfos, la lettre d'information de la FSMP), où intervenaient notamment Vladimir Voevodsky, qui a proposé, avec les fondements univalents, une alternative à la théorie des ensembles comme fondement des mathématiques, ou encore Jean-Yves Girard, un logicien qui a également révolutionné les fondements des mathématiques, dans d’autres directions que Voevodsky.

Q : En lien avec ce sujet, pouvez-vous nous parler un peu du langage COQ ?
PLC : COQ est aussi un langage fondé sur le lambda-calcul, et surtout sur le fait qu’on peut aussi bien écrire un programme (qui calcule quelque chose) qu’écrire une preuve (qui prouve quelque chose). COQ est un assistant de preuve, donc quelque chose d’interactif : en gros, je développe une preuve en COQ, COQ avale ce que je lui donne et me dit si c’est correct - et quand il est content il dit « quid erat demonstrandum ». C’est un objet très fascinant. J’ai travaillé à sa théorie, mais je n’ai jamais mis les mains dans le logiciel proprement dit. Les grands acteurs initiaux de COQ ont été Thierry Coquand pour la partie théorique et Gérard Huet, encore une fois chef d’orchestre et concepteur.

Q : Au final, vous définissez-vous comme informaticien ou comme mathématicien ?
PLC : La majeure partie de mes travaux, et en particulier ceux pour lesquels je reçois ce prix Inria-Académie des Sciences, sont incontestablement de l’informatique, et sont même fondamentaux pour cette discipline. Mais récemment, je me suis intéressé à des questions purement mathématiques, telles que l’étude de structures algébriques à déformation près, grâce à des rencontres notamment avec deux collègues malheureusement disparus depuis : Jean-Louis Loday, spécialiste des opérades, utilisées en topologie et en algèbre, et Patrick Dehornoy, qui m’a entraîné sur des questions d’algèbre effective, de généralisation des groupes de tresses (essayer de trouver des méthodes pour décrire certains groupes avec des générateurs de relations, et étudier les relations entre relations). Certains de mes travaux en mathématiques ont un lien avec l’informatique, le lambda-calcul, mais les plus récents ont un rapport plus lointain avec l’informatique à proprement parler. Plus exactement, ce rapport reste à explorer !

Propos recueillis par Gaël Octavia