  This paper focuses on formally specifying and verifying the chain of formal
semantics of the Esterel synchronous programming language using the Coq proof
assistant. In particular, in addition to the standard logical (LBS) semantics,
constructive semantics (CBS) and constructive state semantics (CSS), we
introduce a novel microstep semantics that gets rid of the Must/Can potential
function pair of the constructive semantics and can be viewed as an abstract
version of Esterel's circuit semantics used by compilers to generate software
code and hardware designs. The paper also provides formal proofs in Coq of the
equivalence beween the CBS and CSS semantics and of the refinement of the CSS
by the microstep semantics.
