Abstract
Compiling Esterel v5
The following lecture presented the compilation of Esterel in software or hardware. Historically, it has gone through several phases: translation of programs into deterministic automata by symbolic computation (with L. Cosserat), translation into much more efficient automata with better causality management (with G. Gonthier, the basis of the first industrialization), then translation into circuits based on constructive semantics which avoids any code explosion. This translation can be seen as the construction, for each program, of a network of proofs grouping together all the constructive proofs of the program for all possible inputs, once again adhering to Curry-Howard's "calculating is proving" paradigm.
For software targets, mathematical semantics and the implementations based on them were decisive factors in Esterel's initial success and its industrialization by CISI-Ingénierie, Simulog and then ILOG. They contributed to the dialogue with users, particularly in avionics (Dassault Aviation). Esterel v5 has been used in communication protocols (Bell Labs, ATT, British Telecom) and robotics (Inria). For circuits, Esterel v5 has been marketed by Synopsys as a component of CAD software for electronic systems: it has been used directly by Cadence Design Systems for joint hardware/software design, and by Intel and Texas Instruments for the specification of control circuits.
