Vérification formelle en Coq de la chaîne des sémantiques pour la compilation d'Esterel