Résumé
Le deuxième cours a porté sur la compilation : la traduction automatique d’un langage de programmation de haut niveau en code exécutable par la machine. Accompagnant l’évolution des langages de programmation, de nombreux algorithmes de compilation et d’optimisation des programmes ont été développés, transformant le code pour en augmenter les performances. Toutes ces transformations ne sont pas sans risque : une erreur dans le compilateur peut lui faire produire du code exécutable faux à partir d’un programme source correct ; on parle alors de mécompilation.
Pour éviter toute mécompilation, il suffit de vérifier formellement le compilateur lui-même, en démontrant que la sémantique du code compilé est fidèle à la sémantique du programme source. C’est un domaine de recherche déjà ancien, avec les premiers travaux de McCarthy et Painter en 1967 et la première vérification mécanisée par Milner et Weyrauch en 1972, mais encore très actif aujourd’hui.
Le cours a exploré cette démarche de vérification sur un compilateur simple (sans optimisations) pour le langage IMP, produisant du code pour une machine virtuelle utilisant une pile. Une première démonstration, utilisant la sémantique naturelle du langage IMP, montre sans trop de peine la préservation de la sémantique des programmes IMP qui terminent.
Pour étendre ce résultat à tous les programmes IMP, y compris ceux qui divergent, nous avons étudié la technique des diagrammes de simulation entre deux sémantiques à réductions. Cependant, la sémantique à réductions d’IMP étudiée au premier cours se prête difficilement à la construction d’un tel diagramme pour notre compilateur. Nous avons donc introduit une autre sémantique à transitions pour IMP, à base de continuations et de réductions sous contexte, en partie inspirée par le focusing en théorie de la démonstration. Cette sémantique permet la construction d’un diagramme de simulation qui montre la préservation sémantique de notre compilateur.
