Martin Andrieux

IRISA, Université de Rennes
Dir. Alan Schmitt

Résumé. Le langage est l’outil de communication le plus élémentaire. Il permet d’exprimer des idées, de les transmettre et de comprendre celles des autres. Si bien que lorsque deux individus ne parlent pas la même langue, ils ont besoin d’un interprète pour échanger. Cette idée se manifeste également en informatique : d’un côté, l’ordinateur comprend une suite d’instructions élémentaires, prenant la forme de code binaire ; de l’autre, les humains écrivent des programmes dans un langage mêlant anglais et mathématiques. Ce rôle de traduction du langage de programmation vers le langage machine est confié au compilateur. De la même manière qu’une erreur de traduction peut causer un quiproquo, une erreur de compilation peut avoir des conséquences graves, en particulier dans des secteurs comme l’aéronautique ou l’énergie. Dans ce contexte, il est essentiel de pouvoir garantir la correction du compilateur, c’est-à-dire que le code que l’on donne à la machine correspond bien à l’idée décrite par le programme. Pour poursuivre l’analogie, on souhaite s’assurer que l’interprète fait correctement son travail. Cette tâche est complexe et multiple : il faut tout d’abord spécifier précisément ce qu’est censé faire le programme (sa sémantique), définir comment du code machine est exécuté, puis montrer que la transformation qu’effectue le compilateur ne contient pas d’erreurs.

Le compilateur CompCert est un exemple de réponse : c’est un compilateur du langage C qui garantit (par une preuve formelle) la correction de la compilation. Cependant, reproduire l’approche de CompCert pour un autre langage représente un énorme travail. À la place, serait-il possible de définir un schéma de compilation générique, qui dépendrait de la sémantique du langage d’entrée ? C’est cette question que cette thèse se propose d’explorer, en passant par une représentation intermédiaire bien étudiée : les machines abstraites. Ces machines modélisent l’exécution d’un programme en faisant abstraction de la complexité d’un ordinateur réel, reliant naturellement les descriptions mathématiques à l’exécution du code. La thèse s’intéressera ainsi à la dérivation certifiée correcte de machines abstraites pour les langages de programmations, puis à l’utilisation de ces machines pour compiler un programme donné.

Motivation

« Mon intérêt pour l’informatique se développe en classe préparatoire, au moment où j’ai mon premier ordinateur personnel. Plus qu’un simple outil, cette machine devient le support de nombreuses expérimentations logicielles qui m’incitent à approfondir ma compréhension de l’objet. Je découvre alors la programmation à travers des projets récréatifs dans différents langages, dont j’explore les différences. Je réalise qu’elles sont souvent plusieurs représentations d’une même idée générale. Je découvre quelques travaux théoriques en recherche informatique. Au moment des concours, mon objectif est déjà la recherche, et l’ENS est mon premier vœu.

À l’ENS, je m’immerge dans cet univers, en particulier à travers plusieurs stages qui me permettent de découvrir différents laboratoires et d’échanger avec des chercheurs passionnés. Initialement intéressé par la compilation (traduction d’un programme source en une suite d’instructions machines), je m’oriente vers des aspects plus formels, avec la volonté de rendre ces concepts applicables à des langages concrets. Les machines abstraites illustrent cette double vocation : cibles de compilation et outils de raisonnement sur les programmes. Leur combinaison avec des recherches récentes sur la représentation des effets promet des résultats riches et profonds. 

Ces motivations m’ont mené, avec mon encadrant, à l’élaboration de ce sujet de thèse visant à étendre le modèle des machines abstraites en vue d’une compilation certifiée et générique. L’équipe EPICURE de l’IRISA, qui réunit des experts du domaine, s’est naturellement imposée pour réaliser ma thèse. »

Parcours

« Après une classe préparatoire scientifique, j’ai intégré sur concours le département Informatique de l’ENS Rennes. J’y ai achevé ma licence Science Informatique, par un stage au Laboratoire d’Informatique du Parallélisme à l’ENS de Lyon, sous la direction de Gabriel Radanne et Ludovic Henrio. Ce travail a mené à la publication d’un papier intitulé «  Active Objects Based on Algebraic Effects ».

J’ai poursuivi en M1 SIF à l ’ENS Rennes, pendant lequel j’ai eu la chance de travailler sur la sémantique du langage Python, sous la direction d’Alan Schmitt, à l’IRISA. Cette année à renforcé ma volonté de faire de la recherche et  le monde académique. Elle m’a également permis l’écriture d’un papier « Skeletal Semantics of a Fragment of Python ». J’ai ensuite effectué un stage en Pologne, sous la direction de Dariusz Biernacki, portant sur un prolongement du travail initié à Rennes autour d’un outil de synthèse de machines abstraites, appliqués aux sémantiques squelettiques.

En 2e année de Master, j’ai souhaité consolider mes connaissances dans les différentes branches de l’informatique en préparant l’agrégation d’informatique. Cela m’a également permis de développer mes compétences à l’oral et ma rigueur pédagogique. Admis au concours, j’ai pu me concentrer sur mon année de M2 Recherche SIF. Dans ce cadre j’effectue alors un stage de recherche de six mois avec Alan Schmitt visant à prolonger et généraliser les travaux engagés en M1. »