Marie Kerjean et la correspondance preuve/programme

Quel est votre domaine de recherche ?

Marie Kerjean : Mon travail de recherche se situe en logique. Je m’intéresse principalement à l’interprétation de certaines preuves comme des fonctions mathématiques, et à ce que cela peut apporter à la théorie des langages de programmation.

Cela consiste à regarder les preuves comme des objets abstraits, et à les comprendre comme des fonctions entre certains espaces, qui eux interprètent les formules. Ça nous permet parfois de découvrir de nouvelles structures mathématiques, ou de nouvelles manières de faire des preuves. Ainsi, ma communauté de recherche a pu comprendre ce qu’était une preuve linéaire, et même ce que voulait dire différencier une preuve ! C’est particulièrement intéressant quand on considère une preuve non pas comme quelque chose qui va décrire ce qui est vrai ou faux, mais comme quelque chose qui va décrire le comportement d’un programme. Grâce à la célèbre correspondance de Curry-Howard, qui type un programme par une preuve, on peut dire que mieux comprendre la logique c’est aussi mieux comprendre les programmes.

Une autre partie plus récente de mon travail consiste à utiliser cette correspondance preuve/programme pour formaliser les mathématiques via un assistant à la preuve. Cela a un intérêt pour vérifier les programmes qui utilisent ces théories mathématiques, mais aussi pour les mathématiciennes et les mathématiciens qui feraient plus confiance à un ordinateur qu’aux vérifications sur papier de leurs preuves.

Qu’avez-vous fait avant d’entrer au CNRS ? Pourquoi avoir choisi le CNRS ? 

M. K. : J’ai fait une thèse à l'Université Paris-Diderot sur la sémantique de la logique linéaire différentielle, sous la direction de Thomas Ehrhard. Pendant ma thèse, j’ai passé deux ans à Copenhague, à l’ITU, au sein d’un groupe qui faisait aussi de la sémantique des preuves mais d’un point de vue un peu différent. À la fin de ma thèse, j’ai changé de sujet et je suis allée à Nantes faire un post-doctorat de deux ans avec Assia Mahboubi, qui est une experte en formalisation des mathématiques, en particulier au sein du projet Mathematical Components. 

À la fin de ces deux ans j’ai eu la chance d’être recrutée au CNRS en informatique. Avoir un poste de chargée de recherche au CNRS est un privilège qui me permet d’avoir la très grande liberté de faire beaucoup de recherche, de prendre des risques et d’avoir le temps de construire des idées nouvelles.  

Qu’est-ce qui vous a amené à faire de l’informatique et/ou des sciences du numérique ? 

M. K. : J’avais lu au lycée sur des articles de vulgarisation en logique qui m’avaient donné envie d’aller vers la recherche en mathématiques. Ce n’est qu’à l’ENS Lyon que j’ai compris que la recherche en informatique existait aussi, et que la logique en faisait partie. Ça m’a paru beaucoup plus ludique et nouveau que ce qu’on étudiait en mathématiques. Et c’est vrai : l’informatique théorique est absolument passionnante et permet de toucher à beaucoup de domaines nouveaux, dont les applications ne sont jamais loin.