Pierre-Louis Curien, un esprit pionnier récompensé par le Grand Prix Inria - Académie des sciences

À la veille de recevoir cette distinction, Pierre-Louis Curien, directeur de recherche émérite au CNRS, revient sur une longue et belle carrière consacrée à l’informatique théorique, avant tout marquée par des rencontres et des collaborations avec les plus grands noms de la discipline.

Tout commence au milieu des années soixante-dix : élève de l’École normale supérieure (ENS) à Ulm, agrégé de mathématiques, Pierre-Louis Curien hésite pourtant à poursuivre dans cette voie. « J’étais intimidé par les ‘matheux’ de l’ENS… », confie celui qui établira pourtant, tout au long de ses recherches, de nombreux ponts entre algèbre et informatique afin d’en révolutionner certains concepts. « C’est après avoir rencontré Maurice Gross, linguiste et informaticien, pionnier des dictionnaires électroniques, et Gérard Berry, informaticien, titulaire de la chaire ‘’Algorithmes, machines et langages’’ au Collège de France entre 2012 et 2019, que je me lance sur la voie de l’informatique théorique, avec une thèse de doctorat portant sur les modèles du λ calcul (lire lambda-calcul, NDLR). »

Inventé dans les années trente par le logicien Alonzo Church, peu avant la célèbre machine de Turing, le λ-calcul est un langage épuré, correspondant aux fondamentaux de la programmation que sont les déclarations et les appels de procédure. Il constitue de nos jours la charpente des langages de programmation « fonctionnels », appelés ainsi car ils mettent en avant que les programmes sont des fonctions, prenant des entrées et retournant un résultat. Parmi ces langages figure OCaml, fleuron de la recherche française. Principalement développé au sein d’Inria, OCaml est utilisé dans l’enseignement, dans la recherche, où il sert de support à de nombreux développements logiciels, et dans l’industrie, dans des domaines aussi divers que les systèmes embarqués ou l’informatique financière.

« Mes premières recherches visaient à répondre à des questions théoriques : comment montrer qu’un programme réalise bien une tâche donnée ? Est-ce que deux programmes différents codés pour accomplir une même tâche le font avec la même précision – et comment l’évaluer ? », explique Pierre-Louis Curien. Ces problèmes intéressent tout d’abord les concepteurs de langages de programmation, par exemple pour s’assurer de leur efficacité et de leur fiabilité.

 « J’ai montré qu’on peut rigoureusement répondre à ces questions en formalisant de façon mathématique le fonctionnement d’un programme informatique, en particulier à l’aide de concepts issus de l’algèbre », résume le chercheur. Pierre-Louis Curien n’a cessé de déployer une créativité apparemment sans limites, afin de creuser ce lien entre mathématiques et informatique. Dans les années 1980-1990, ses recherches ont eu des retombées pour la conception et l’implantation des langages de programmation.

Elles ont abouti en particulier à la création de machines virtuelles, comme la CAM (categorical abstract machine). Cette « machine abstraite catégorique » a constitué le cœur du premier compilateur du langage CAML, devenu plus tard Ocaml. « Le changement de point de vue était saisissant : les structures très abstraites dans lesquelles s’interprète le λ-calcul se révélaient être un langage ‘‘de bas niveau’’, c’est-à-dire proche du langage machine, et l’interprétation devenait une compilation », commente le chercheur.

Depuis les années 2000, Pierre-Louis Curien s’est intéressé aux fondements logiques des « assistants de preuve », dont les applications sont la certification des programmes et la formalisation des preuves mathématiques. Le premier domaine est d’une importance majeure pour la sûreté des logiciels, comme en informatique embarquée : il a par exemple été établi que l’explosion d’Ariane 5 en 1996 était due à l’exécution d’un code devenu inutile pour ce lanceur. Le second répond aux besoins de la communauté mathématique de disposer d’outils de vérification de démonstrations complexes.

La contribution de Pierre-Louis Curien à sa discipline s’étend bien au-delà de la recherche et bénéficie à l’ensemble de sa communauté scientifique. Il a en effet contribué à fonder puis à animer un laboratoire CNRS et une équipe de recherche Inria, regroupant mathématiciens et informaticiens, ainsi qu’un département de recherche et d’enseignement à l’ENS. Il a aussi animé ou participé à une trentaine de projets de recherche collaborative, dirigé une vingtaine de thèses, publié une cinquantaine d’articles et ouvrages scientifiques et siégé dans de nombreuses instances d’administration scientifique nationale.

Avec ce Grand Prix Inria – Académie des sciences, Pierre-Louis Curien rejoint le groupe prestigieux des grands chercheurs français de l’informatique et y retrouve des figures familières, tels Gérard Huet, membre de l'Académie des sciences, ou Xavier Leroy, professeur au Collège de France. En informatique, comme dans une vie d’homme peut-être, tout est question de rencontres !