Vers la certification du compilateur v5 d'Esterel dans Coq

Le compilateur v5 d'Esterel est basé sur un raffinement sémantique de la causalité correspondant aux «circuits constructifs» dans le domaine du matériel. La sémantique est présentée par un ensemble de règles d'inférence dans le style de la sémantique naturelle. Nous avons prouvé formellement la correction de la traduction d'une partie significative du langage en circuits au moyen du système de preuves Coq et de son interface utilisateur disponible dans Centaur. La nouvelle sémantique constructive d'Esterel a d'abord été écrite en Typol, donnant d'une part un interprète en Prolog et d'autre part une spécification en Coq. La traduction en circuit à la base du compilateur Esterel v5 a été directement spécifiée en Coq en utilisant l'ordre supérieur. Le principal travail a consisté à certifier le compilateur v5 en Coq en raisonnant sur ces spécifications.