Cette lettre est d'abord l'occasion de revenir sur la grande annonce de la semaine dernière qui a vu Pierre-Louis Curien se voir décerner le Grand prix Inria – Académie des sciences. Un zoom spécifique est décerné à cette reconnaissance très prestigieuse d'un de nos membres, auquel je me permets d'ajouter quelques mots personnels dans cet édito.

Si Pierre-Louis est un visionnaire, c'est aussi un bâtisseur de communautés et un inspirateur pour beaucoup. Je l'ai rencontré «vraiment» la première fois lors d'un repas (copieux et arrosé) organisé pour me conter l'histoire du laboratoire PPS. A l'issue de ce repas, j'ai été fasciné, et presque jaloux, par la vision qu'avait eu Pierre-Louis en créant PPS, puis le projet Inria π.r2. Je suis heureux de voir PPS continuer d'exister au sein de l'IRIF dans une structure favorable à ses échanges uniques. En lisant cette sélection de brèves liées à son prix, j'ai (re)-découvert son parcours qui inspireront les plus jeunes, car le parcours de Pierre-Louis est avant tout humain avec doutes, hésitations et passions. J'ai aussi appris plus sur ses grandes découvertes, remarquables et uniques. J'ai hâte comme beaucoup d'entre vous de fêter cela le moment venu par un pot mémorable à l'IRIF !

Retrouvez aussi dans cette lettre les chantiers importants de l'IRIF concernant notre vie en commun à savoir le lancement du mentorat, et l'élaboration d'une charte des membres de l'IRIF. Après être passée par la commission égalité femmes-hommes, les conseils de direction et du laboratoire, la charte vous est maintenant présentée à tous. Vous pouvez exprimer vos réactions au sein de vos équipes ou pôles, ainsi que via un formulaire anonyme.

L'assemblée générale de l'IRIF, programmée pour le 12 janvier 13h-15h, sera l'occasion de valider définitivement cette charte, ainsi que de revenir sur d'autres actions de ce semestre, et des chantiers du suivant, dans le contexte actuel si particulier.

Enfin, ne manquez pas la semaine prochaine le workshop Species and Operads in Combinatorics and Semantics (SOCS2020) organisé par l'IRIF.

• Le conseil de laboratoire du 1er décembre a validé à l'unanimité, moins une abstention, la charte des membres de l'IRIF dans sa version du 01/12/2020, et recommande avant son adoption définitive de :
  • Faire circuler le projet de charte parmi les membres de l'IRIF
  • Encourager des discussions au sein des équipes thématiques et pôles
  • Recueillir les avis via un formulaire anonyme

• Charte des membres de l'IRIF
  • Charte des membres de l'IRIF dans sa version du 01/12/2020
  • Formulaire pour exprimer son opinion

• Mentorat. Qu'est ce que le mentorat ? Comment cela s'organise à l'IRIF ? Qui contacter pour en parler ? L'intranet s'enrichit d'une page explicative Le mentorat sur le dispositif de mentorat nouvellement mis en place au laboratoire.

• Assemblée général de l'IRIF, 12 janvier 13h-15h (en ligne)

• Concours chercheurs et chercheuses CNRS 2021
  • Ouvert jusqu'au 7 janvier 2021 13h
  • Liste des offres : la recherche à l'IRIF est couverte par les sections 6, 41 et 51

• Inventaire matériel empruntable pour le télétravail (disponible au secrétariat - bureau 4001- ou dans le bureau de Houy)
  • Tablette graphique : 9
  • iPad : 3
  • Stylet pour Ipad : 2
  • Webcam : 5
  • Casque-micro : 4
  • Ecran : 3
  • Ordinateurs : 3
  • Adaptateurs divers

• December 10-11, IRIF is co-organizing SOCS2020, a workshop on Species and Operads in Combinatorics and Semantics. This event will gather two very active communities in Paris area and beyond, the combinatorics and semantics communities, around a common tool: species and operads theory. More information.

Pierre-Louis Curien, directeur de recherche émérite CNRS à l’IRIF, reçoit le Grand Prix Inria – Académie des sciences.

Le grand prix Inria récompense un.e scientifique ou un ensemble de scientifiques ou une équipe de recherche ayant contribué de manière exceptionnelle au champ des sciences informatiques et mathématiques.

Pierre-Louis Curien est spécialiste de la théorie (ou sémantique) des langages de programmation. Ses travaux avec Gérard Berry ont donné un statut mathématique au contrôle de l’exécution des programmes (en plus de leur seul comportement d’entrée-sortie). Il a par la suite œuvré à l’introduction d’abstractions mathématiques dans son domaine. Une application spectaculaire en a été la conception de la machine abstraite catégorique (CAM), qui a donné son nom au langage de programmation OCaml. Bougeant inlassablement les lignes, il applique aujourd’hui sa boîte à outils syntaxique aux structures algébriques à homotopie près qui émergent en mathématiques dites fondamentales.

Portait en vidéo de l'Université de Paris

Interview de la FSMP (extrait des propos de Pierre-Louis sur sa contribution dans OCaml)

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.

Interview de La Recherche (extrait des propos de Pierre-Louis sur ses contributions liées à la correspondance de Curry-Howard)

La correspondance de Curry-Howard issue de travaux sur la logique stipule qu’en utilisant les langages des types, les preuves mathématiques peuvent se lire comme des programmes. […] À la recherche d’un formalisme qui fonctionne pour représenter à la fois preuves mathématiques et programmes, Thierry Coquand, Gérard Huet et Christine Paulin ont conçu le langage Coq qui permettra des progrès énormes en vérification assistée par ordinateur (d’autres langages de vérification existent, mais Coq est l’un des plus répandus). C’est un sujet passionnant et je me suis mis à étudier les structures mathématiques non seulement pour les programmes, mais aussi pour les preuves. Et j’ai contribué à fédérer cette recherche des assistants de preuve au sein d’un labo et d’une équipe Inria.

Dans mon travail, à la fin des années 1990, j’ai notamment mis en évidence, en étudiant la substitution dans les types, que regarder les types à déformation près (ce qu’on nomme homotopie) était le bon point de vue. Est alors arrivé un mathématicien génial – Vladimir Voïevodski – qui a eu l’idée d’en faire une théorie globale. Autrement dit, la théorie des types et la correspondance de Curry-Howard ne permettent pas seulement de faire des assistants de preuve, qui prouvent des résultats mathématiques ou des programmes, mais ils autoriseraient une refondation des mathématiques sur cette notion de type (plutôt que sur la notion d’ensemble). Et à l’inverse, la théorie des types homotopiques a aussi des implications sur les assistants de preuve, sur les langages de programmation. Par exemple du point de vue des langages, cela devrait donner lieu à de nouvelles façons de comprendre quand deux programmes font la même chose. Ou quand deux types de données qui ont des représentations très différentes en machine sont en fait intertraduisibles.

Article d'Inria sur le prix et Portrait d'Inria de Pierre-Louis (extraits sur son impact sur la communauté)

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 (1999, PPS) et une équipe de recherche Inria (2009, π.r2), regroupant mathématiciens et informaticiens, ainsi qu’un département de recherche et d’enseignement à l’ENS (1987).

L'équipe-projet pi-r2 qu'il a fondée avec Hugo Herbelin joue depuis sa création un rôle majeur dans la conception, le développement et la maintenance de Coq. Pierre-Louis Curien s'est par ailleurs beaucoup engagé dans les débats profonds qui ont préparé la création de l'INS2I au CNRS, menant pour la première fois en France à une définition de l'informatique en tant que domaine scientifique.

• ERC : Le calendrier officiel
  • ERC Starting Grant 2021 (thèse obtenue entre 01/01/2014 et 31/12/2018) : deadline 09 mars 2021
  • ERC Consolidator 2021 (thèse obtenue en 01/01/2009 et 31/12/2013) : deadline 20 avril 2021
  • ERC Advanced 2021 (thèse obtenue avant le 01/01/2009) : deadline 31 août 2021
  • Plus d'information

• FSMP : Bourses de thèse du Cofund MathInParis2020 ouvert uniquement à des candidats n'ayant pas passé plus de 12 mois en France dans les 3 ans précédant la fermeture de l'appel d'offre. Deadline 13/2/2021.

• Ile de France : La Région lance son 2ème appel pour propositions de thèse en lien avec des entreprisesdans le cadre de l'appel à projet Paris Région PhD 2021. Plus d'information.

• Newsletter des partenaires : Les lettres arrivent sporadiquement aux membres de l'IRIF. Elles sont donc listées ci-dessous.
  • CNRS Hebdo du 03/12/2020
  • Université de Paris Infos du 03/12/2020
  • Lettre de l'internationalisation scientifique de l'Université de Paris du 03/12/2020