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

L’exposé a d’abord présenté des preuves en Coq des théorèmes de correspondance reliant les différentes sémantiques de plus en plus précises d’Esterel, telles qu’énoncées dans le livre numérique The Constructive Semantics of Pure Esterel puis affinées dans la thèse d’Olivier Tardieu en 2004 : sémantique logique, sémantique constructive, sémantique par transitions entre états marqués dans les termes. Il a ensuite introduit une nouvelle sémantique opérationnelle réalisant la sémantique constructive par propagation dans le programme de jetons colorés, intuitivement proche de la traduction en circuits mais plus facile à traiter. La preuve de correction et de déterminisme de cette nouvelle sémantique est actuellement limitée aux programmes sans boucle : elle devra être étendue aux programmes généraux en incorporant un des traitements de la réincarnation présentés dans le cours 4 ci-dessus.