Lorsqu'on rencontre le calme Julien, il semble impossible de l'imaginer sur des rollers et encore moins faire du roller-hockey. Et pourtant ! Passionné de Coq, de géométrie et de logique, Julien attache une grande importance à la pédagogie et à la transmission, ainsi qu'à l'interdisciplinarité. Rencontre avec Julien Narboux, nouveau maître de conférence à l'IRIF.

“Ça m'a amené à m'intéresser aux fondements de la géométrie, puis à la frontière avec la démonstration automatique appliquée à la géométrie, avec des sujets connexes tels que comment générer des preuves lisibles ou comment améliorer les systèmes pour que ce soit plus facile de formaliser des preuves.” Julien Narboux, maître de conférence | Pôle Preuves, programmes et systèmes - Équipe Analyse et conception de systèmes et Preuves et programmes.

J'ai fait le DEA Sémantique, Preuves et Programmation à l’Université Paris Diderot/ENS Cachan (aujourd’hui Université Paris Cité). Certains de mes professeurs de l’époque sont désormais des collègues à l’IRIF. J'ai poursuivi en thèse sous la direction d'Hugo Herbelin, en commençant à l’INRIA Rocquencourt, puis nous avons été déplacés sur le plateau de Saclay, dans les locaux du LIX, le Laboratoire d'Informatique de l'Ecole polytechnique.

Ensuite, j'ai fait un post-doc à Munich, dans l'équipe de Tobias Nipkow sur des techniques de formalisation des preuves en présence de lieurs sous la direction de Christian Urban. Pour finir, j'ai été recruté à l'Université de Strasbourg où j'ai été maître de conférences pendant 17 ans. Mon épouse a été mutée à Paris, et j'ai eu la chance de pouvoir muter de mon côté à l’IRIF.

J'ai longtemps travaillé sur la formalisation de la géométrie classique, principalement avec l'assistant de preuve Coq. Ça m'a amené à m'intéresser aux fondements de la géométrie, puis à la frontière avec la démonstration automatique appliquée à la géométrie, avec des sujets connexes tels que comment générer des preuves lisibles ou comment améliorer les systèmes pour que ce soit plus facile de formaliser des preuves.

Et puis, plus récemment, j'ai fait un peu de démonstration automatique, pas forcément liée à la géométrie.

C'est venu un peu par hasard. L'intérêt pour l'informatique et la logique, je l'ai eu assez jeune, au lycée. J'avais lu des choses sur le théorème de Gödel qui m'avaient fascinées. L'intérêt pour la formalisation et démonstration automatique en géométrie est venu un peu par hasard : au moment de commencer ma thèse, j'ai contacté Hugo Herbelin et nous avons discuté ensemble autour d'un café. C’est comme ça qu’est né mon sujet de thèse.

J’ai plusieurs directions. Tout d’abord, je développe avec Predrag Janičić, depuis deux-trois ans, un démonstrateur automatique basé sur un fragment de la logique du premier ordre, qui s'appelle la logique cohérente. Il y a d'autres chercheurs-ses à l’IRIF qui s’intéressent à ce fragment, c’est pourquoi j'aimerais continuer dans cette lignée. Et puis, pour l'instant, notre prouveur automatique n'est pas encore relié à Coq, donc l'idée serait de l'adapter afin de pouvoir l'utiliser avec cet assistant de preuve.

Récemment, j'ai encadré une stagiaire avec laquelle on essayait de faire de la formalisation automatique d’énoncés donnés en langue naturelle. J'aimerais continuer dans cette direction à travailler sur les rapports entre la langue naturelle et la langue formelle, notamment appliqués à l'enseignement. Hugo Herbelin travaille justement là-dessus, ainsi que Paul-André Melliès et Santiago Arambillete, un doctorant.

Je participe aussi au projet ANR APPAM qui a commencé en janvier dernier, qui porte justement sur l'utilisation des assistants de preuves pour l'enseignement. Dans ce cadre-là, j'encadrais le post-doc de Evmorfia-Iro Bartzia, qui a été recrutée maîtresse de conférences au LDAR, le laboratoire de Didactique André Revuz. Je vais donc naturellement pouvoir collaborer avec elle sur cette thématique, éventuellement avec d’autres membres de l’IRIF qui s'intéressent à ces questions et avec les mathématiciens qui enseignent déjà la démonstration avec un assistant de preuve.

Enfin, je vais continuer de co-encadrer Frédéric Tran-Minh, avec Laure Gonnord, un doctorant que je suis à distance (il est à Valence) et qui travaille sur cette même thématique.

Récemment, je me suis intéressé à la didactique : j'ai collaboré avec des didacticiens des maths, et je trouve que ce lien avec des personnes d'autres disciplines est intéressant. Il m’arrive aussi d'aller à des conférences sur la philosophie des mathématiques, par exemple. J’aimerais beaucoup travailler sur de l'interdisciplinarité avec les logiciens, à la frontière logique - philosophie/didactique. La proximité du laboratoire SPHERE est une opportunité.

J'ai commencé avec la Fête de la Science, en lançant dans mon laboratoire à Strasbourg, un groupe de travail sur cet événement. L'idée était aussi d’encourager les chercheurs à se parler entre équipes. Nous avons donc fait un stand pour cet événement, sur l'informatique en général, en proposant des activités d'informatique débranchée. Au fil des années, nous avons continué à monter des ateliers pour la Fête de la Science.

J'ai également participé à plusieurs Pint of Science, sous différents formats : des conférences, des activités débranchées ou un mélange des deux.

Avec des collègues, nous avons aussi participé aux décodeuses d’informatique à travers les Cordées de la réussite. On voulait travailler sur l'égalité fille-garçon en informatique en allant à la rencontre des élèves, avant qu'ils ne fassent leurs choix d’orientation. J'ai géré ce projet pendant trois ou quatre ans, on visitait 20 à 30 classes par an : c’est ce que j’appelais le match aller, puisqu’on se rendait dans les établissements pour faire ces ateliers. Notre parti-pris était de ne pas s’adresser seulement aux filles puisque nous voulions également provoquer un éveil sur ce qu'est l'informatique en général, casser les préjugés sur l'informatique. On s’appuyait néanmoins sur des biais des IA par exemple en prenant des exemples où il y a des problèmes d'égalité de genre. Ensuite, c’est ce que j’appelle donc le match retour, nous les invitions à venir à l'université : on proposait une conférence scientifique de vulgarisation accompagnée d’ateliers d'informatique débranchés. Comme il devenait difficile de répondre à la demande, nous avons développé une antenne de la cordée à Mulhouse, en transmettant le flambeau aux collègues de l’UHA, Université Haute-Alsace. Lors d’une formation, nous avons également rencontré des élèves polytechniciens, qui, parce qu'étrangers ne pouvaient pas faire de service militaire, réalisaient donc un service civique dans des collèges. Ils ont eux-mêmes créé une cordée polytechnique.

A Strasbourg, j’ai également participé à la conception d’une exposition permanente en collaboration avec Raphael Vandamme pour le Vaisseau, un musée des sciences pour les enfants. Ils voulaient remettre au goût du jour une partie de leur exposition permanente en faisant un focus sur la thématique des robots et de l'intelligence artificielle. Avec un collègue, Basile Sauvage, nous les avons accompagnés. Il y a quelques années, ils avaient fait une exposition temporaire sur l'IA et on avait essayé de leur donner des billes sur ces sujets et nous les avions formé à l'informatique débranchée. C'était une super aventure, parce qu'on a travaillé avec un muséographe, des communicants, des graphistes, des designers… Notre leitmotiv était vraiment de pouvoir toucher un maximum de personnes.

J'ai aussi pris part aux Maths C2+, qui sont des stages d'une semaine pour des élèves de seconde, sur la base du volontariat, pour des élèves motivés par les maths et l'informatique. Pendant une heure et demie tous les matins, ils étudient un problème ouvert de maths qui est à leur niveau, où ils doivent réfléchir, essayer des exemples et, à la fin de la semaine, ils font un exposé sur ce qu'ils ont pu trouver pour résoudre leur problème. Nous leur proposions également des exercices d'informatique débranchée ou des conférences par exemple. J'ai d’ailleurs pour projet d'en refaire.
En fait, dans le cas de notre projet ANR sur l'utilisation des assistants de preuve pour l'enseignement, nous aimerions tester de faire faire du Coq à des lycéens. Une collègue-chercheuse, qui s'appelle Micaela Mayero qui est à l’Institut Galilée - Université Paris Nord, a déjà fait ça dans le cadre d'un stage maths C2+, et je pense que c'est une bonne façon de faire une expérimentation avec des secondes sans que ça ne soit trop compliqué.

Lors de ma première conférence internationale, pendant le dîner de gala qui était commun avec une autre conférence, je me suis retrouvé par le hasard du placement à côté d'un vieux monsieur qui m'a gentiment demandé quel était mon domaine de recherche. Je lui ai également demandé quel était le sien, il m'a répondu la complexité et la calculabilité. Ce n’est que le lendemain que je me suis rendu compte que c'était Stephen Cook, celui du théorème qui m’avait tant impressionné quelques années avant.

J'aime bien faire du roller et récemment je me suis mis au roller-hockey. Pendant ma thèse, je faisais des rando-roller le vendredi soir et je vais peut-être revenir faire des rando-roller 17 ans après !
Le roller-hockey se pratique en gymnase, et il y en a justement un, juste à côté de l’IRIF. J'ai commencé ce sport par hasard à 42 ans, c'est d’ailleurs un peu bizarre d’être débutant de roller-Hockey à cet âge. Je cherchais une activité pour mes enfants et j'ai vu qu'il y avait des cours d'initiation au roller qui étaient sur des créneaux partagés tout âge, adulte et enfant. Je me suis dit que je pouvais me remettre à faire du roller tout en faisant du sport avec mon fils. Au bout de deux ans d'initiation, le coach m’a proposé d’essayer le roller-hockey. C’est comme ça que j’ai commencé.

2024 : Arrivée à l'IRIF en tant que maître de conférences
2007 : Maître de conférences à l'Université de Strasbourg
2006-2007 : Post-doc encadré par Christian Urban
2002-2006 : Thèse encadrée par Hugo Herbelin