Compilation formellement vérifiée d'un langage pour le calcul formel

Dans cet article, nous présentons une ébauche de langage de bas niveau ayant pour but de pouvoir écrire les algorithmes de base du calcul formel. Les structures de données manipulées par ces algorithmes étant principalement des tableaux, c'est sur ces derniers que notre langage se concentre. Nous présentons sa sémantique qui a été formalisée en Coq. Elle a été conçue dans l'optique d'être sûre, en éliminant certains comportements indéfinis tels que l'accès en dehors des bornes d'un tableau. Un autre objectif de cette sémantique est de simplifier la preuve de programme, par exemple en distinguant tableaux mutables et immuables. Nous nous intéressons enfin à la compilation formellement vérifiée de ce langage vers un langage assembleur. Pour atteindre cet objectif, nous avons écrit un compilateur de notre langage vers le langage intermédiaire Clight de CompCert et nous avons prouvé formellement la préservation de la sémantique lors de cette traduction