Abstract
The talk first presented Coq proofs of correspondence theorems linking Esterel's various increasingly precise semantics, as set out in the digital book The Constructive Semantics of Pure Esterel and then refined in Olivier Tardieu's 2004 thesis: logical semantics, constructive semantics, semantics by transitions between marked states in terms. He then introduced a new operational semantics realizing constructive semantics by propagation in the colored token program, intuitively close to the circuit translation but easier to process. The proof of correctness and determinism of this new semantics is currently limited to loop-free programs: it will have to be extended to general programs by incorporating one of the reincarnation treatments presented in lecture 4 above.
