Compilation Générique Certifiée par Machines Abstraites

La certification d'un compilateur est une tâche extrêmement complexe. Il s'agit en effet de prouver formellement que le comportement du programme compilé fait partie des comportements possibles du programme source. Le compilateur CompCert illustre le travail considérable que cela représente : il nécessite la définition de 10 langages différents et les preuves que les transformations entre ces langages sont correctes. Le cœur de la certification d'un compilateur est ainsi la définition de sémantiques et de transformations entre ces sémantiques. De plus, ce lourd travail est à accomplir de nouveau pour chaque langage considéré.

Pour pallier ce problème, plusieurs approches ont proposé de systématiquement dériver des machines abstraites à partir de la définition de la sémantique d’un langage, puis de s’appuyer sur cette dérivation pour définir un compilateur pour le langage considéré. Ces approches souffrent de trois défauts. Tout d’abord, elles ne considèrent que des langages très simples (définis en une dizaine de règles) et il n’est pas clair qu’elles puissent passer à l’échelle. Pour donner un ordre de grandeur, la spécification formelle JSCert d’un sous-ensemble de JavaScript de 2014 comprenait environ 1000 règles. Ensuite, les approches ne traitent pas de fonctionnalités sémantiques complexes comme la gestion de continuations, qui est nécessaire pour compiler des générateurs (JavaScript ou Python) et des effets algébriques (OCaml 5). Enfin, ces approches ne considèrent pas la certification du compilateur obtenu, que ce soit en produisant un certificat pour un langage donné ou en prouvant directement la dérivation.

Le but du sujet de thèse que nous proposons est de définir une technique de compilation générique par des machines abstraites qui passe à l’échelle, qui gère les effets complexes comme les continuations et qui soit certifiée. La description des différents langages pourra s’appuyer sur nos précédents travaux sur le méta-langage Skel. La candidate ou le candidat choisissant ce sujet sera hébergé dans l’équipe Épicure, qui réunit les compétences en sémantiques de langages, en machines abstraites et en compilation.