C. André, SyncCharts: A visual representation of reactive behaviors. RR 95-52, I3S, 1995.

C. André, Representation and analysis of reactive behaviors: A synchronous approach, Proc. CESA'96, pp.19-29, 1996.

A. V. Aho, R. Sethi, and J. D. Ullman, Compilers: principles, techniques, and tools, 1986.

P. Henk and . Barendregt, The Lambda Calculus, Its Syntax and Semantics, of Studies in Logics and the Foundations of Mathematics, 1981.

A. Benveniste and G. Berry, The synchronous approach to reactive realtime systems Another Look at Real Time Programming, Proceedings of the IEEE, pp.1270-1282, 1991.

[. Berry and L. Cosserat, The ESTEREL synchronous programming language and its mathematical semantics, Seminar on Concurrency, pp.389-448, 1984.
DOI : 10.1007/3-540-15670-4_19
URL : https://hal.archives-ouvertes.fr/inria-00076230

P. Borras, D. Clément, T. Despeyroux, J. Incerpi, G. Kahn et al., Centaur: the system, Proc. SDE'88, pp.14-24, 1988.
URL : https://hal.archives-ouvertes.fr/inria-00075774

A. Benveniste, P. Caspi, S. Edwards, N. Halbwachs, P. L. Guernic et al., The synchronous languages twelve years later, Proceedings of the IEEE, Special issue on Embedded Systems, pp.64-83, 2003.

S. Bensalem and P. Caspi, Catherine Parent-Vigouroux, and Cécile Dumas Canovas. A methodology for proving control systems with Lustre and PVS, Proc. DCCA'99, pp.89-107, 1999.

[. Boussinot, R. De, and S. , The Esterel language. Another Look at Real Time Programming, Proceedings of the IEEE, pp.1293-1304, 1991.
URL : https://hal.archives-ouvertes.fr/inria-00075075

[. Boussinot, R. De, and S. , The SL synchronous language, IEEE Transactions on Software Engineering, vol.22, issue.4, 1995.
DOI : 10.1109/32.491649
URL : https://hal.archives-ouvertes.fr/inria-00074168

[. Berry, Real-time programming: General purpose or special-purpose languages, Information Processing, pp.11-17, 1989.
URL : https://hal.archives-ouvertes.fr/inria-00075494

Y. Bertot, Implementation of an interpreter for a parallel language in centaur, Proc. ESOP'90, pp.57-69, 1990.
DOI : 10.1007/3-540-52592-0_55
URL : https://hal.archives-ouvertes.fr/inria-00075483

G. Berry, Esterel on hardware, Mechanized reasoning and hardware design, pp.87-104, 1992.

[. Berry, Preemption in concurrent systems, Proc. FSTTCS'93, pp.72-93, 1993.
DOI : 10.1007/3-540-57529-4_44

[. Berry, The Semantics of Pure Esterel, Program Design Calculi of Series F: Computer and System Sciences NATO ASI Series, pp.361-409, 1993.
DOI : 10.1007/978-3-662-02880-3_12

[. Berry, The Constructive Semantics of Pure Esterel. INRIA, 1999.

[. Berry, The Esterel Language Primer v5 91, INRIA, 2000.

[. Berry and G. Gonthier, The Esterel synchronous programming language: design, semantics, implementation, Science of Computer Programming, vol.19, issue.2, pp.87-152, 1992.
DOI : 10.1016/0167-6423(92)90005-V
URL : https://hal.archives-ouvertes.fr/inria-00075711

S. Boulmé and G. Hamon, Certifying Synchrony for Free, Proc. LPAR'01, pp.495-506
DOI : 10.1007/3-540-45653-8_34

A. Bouali and . Xeve, Xeve, an Esterel verification environment, Proc. CAV'98, pp.500-504, 1998.
DOI : 10.1007/BFb0028770
URL : https://hal.archives-ouvertes.fr/inria-00069957

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/inria-00528590

M. Daniel and . Chapiro, Globally-asynchronous locally-synchronous systems (performance , reliability, digital), 1985.

D. Clément and J. Incerpi, Programming the behavior of graphical objects using Esterel, Proc. TAPSOFT'89, 1989.

P. Caspi and M. Pouzet, Lucid Synchrone: une extension fonctionnelle de Lustre, Proc. JFLA'99. INRIA, 1999.

E. Closse, M. Poize, J. Pulou, P. Venier, and D. Weil, Saxo???rt: Interpreting Esterel Semantic on a Sequential Execution Structure, Proc. SLAP'02, 2002.
DOI : 10.1016/S1571-0661(05)80443-8

A. Maulik and . Dave, Compiler verification: a bibliography, SIGSOFT Softw. Eng. Notes, vol.28, issue.6, pp.2-2, 2003.

G. Nicolaas and . De-bruijn, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, Indag. Math, vol.34, pp.381-392, 1972.

W. Edsger and . Dijkstra, Go To statement considered harmful, Comm. ACM, vol.11, issue.3, pp.147-148, 1968.

P. Bruce and . Douglass, Real-Time UML: Developing Efficient Objects for Embedded Systems, 1997.

A. Stephen and . Edwards, Languages for Digital Embedded Systems, 2000.

A. Stephen, V. Edwards, M. Kapadia, and . Halas, Compiling Esterel into static discrete-event code, Proc. SLAP'04, Electronic Notes in Theoretical Computer Science, 2004.

X. Fornari, Optimisation du contrôle et implantation en circuits de programmes Esterel, 1995.

M. L. Paul-le-guernic, T. Borgne, C. L. Gauthier, and M. , Programming real time applications with Signal. Another Look at Real Time Programming, Proceedings of the IEEE, p.79, 1991.

S. David and . Gladstein, Compiler correctness for concurrent languages, 1994.

[. Grandpierre, C. Lavarenne, and Y. Sorel, Optimized rapid prototyping for real-time embedded heterogeneous multiprocessors, Proceedings of the seventh international workshop on Hardware/software codesign , CODES '99, pp.74-78, 1999.
DOI : 10.1145/301177.301489

J. C. Michael, T. F. Gordon, and . Melham, Introduction to HOL: a theorem proving environment for higher order logic, 1993.

[. Gonthier, Sémantique et modèles d'exécution des langages réactifs synchrones: applicationàapplicationà Esterel, 1988.

J. F. Groote, Transition system specifications with negative premises, Proc. CONCUR'90, pp.332-341
DOI : 10.1007/BFb0039069

[. Halbwachs, Synchronous Programming of Reactive Systems, 1993.

D. Harel, Statecharts: a visual formalism for complex systems, Science of Computer Programming, vol.8, issue.3, pp.231-274, 1987.
DOI : 10.1016/0167-6423(87)90035-9

N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, The synchronous dataflow programming language Lustre. Another Look at Real Time Programming, Proceedings of the IEEE, pp.1305-1320, 1991.

[. Halbwachs, F. Lagnier, and C. Ratel, Programming and verifying real-time systems by means of the synchronous data-flow language LUSTRE, IEEE Transactions on Software Engineering, vol.18, issue.9, pp.785-793, 1992.
DOI : 10.1109/32.159839

D. Harel and A. Pnueli, On the Development of Reactive Systems, Logics and models of concurrent systems, pp.477-498, 1985.
DOI : 10.1007/978-3-642-82453-1_17

[. Standard, VHDL Language Reference Manual, IEEE Std, pp.1076-1993, 1994.

G. Kahn, Natural semantics, Proc. STACS'87, pp.22-39, 1987.
DOI : 10.1007/BFb0039592
URL : https://hal.archives-ouvertes.fr/inria-00075953

C. Stephen and . Kleene, Representation of events in nerve nets and finite automata, Automata Studies, pp.3-41, 1956.

M. Kerboeuf, D. Nowak, and J. Talpin, Specification and Verification of a Steam-Boiler with Signal-Coq, Proc. TPHOLs'00, pp.356-371, 2000.
DOI : 10.1007/3-540-44659-1_22
URL : https://hal.archives-ouvertes.fr/hal-00544631

X. Leroy, The Objective Caml system, release 3.06, 2002.

[. Lanusse, S. Gérard, and F. Terrier, Real-Time Modeling with UML: The ACCORD Approach, Proc. UML'98, pp.319-335, 1998.
DOI : 10.1007/978-3-540-48480-6_25

F. Maraninchi, The Argos language: Graphical representation of automata and description of reactive systems, Proc. IEEE Conf. on Visual LanguagesMig94] Frédéric Mignard. Compilation du langage Esterel en systèmes d'´ equations booléennes, 1991.

R. Milner, Communication and Concurrency. Series in Computer Science, 1989.

L. Morel, Efficient compilation of array iterators for Lustre, Proc. SLAP'02, 2002.
DOI : 10.1016/S1571-0661(05)80437-2
URL : https://hal.archives-ouvertes.fr/hal-00387350

L. John, J. Mccarthy, and . Painter, Correctness of a compiler for arithmetic expressions, Proceedings Symposium in Applied Mathematics, pp.33-41, 1967.

H. Marchand, E. Rutten, M. L. Borgne, and M. Samaan, Formal verification of programs specified with signal: application to a power transformer station controller, Science of Computer Programming, vol.41, issue.1, pp.85-104, 2001.
DOI : 10.1016/S0167-6423(00)00020-4
URL : https://hal.archives-ouvertes.fr/inria-00526287

D. Nowak, J. Beauvais, and J. Talpin, Co-inductive axiomatization of a synchronous language, Proc. TPHOLs'98, pp.387-399, 1998.
DOI : 10.1007/BFb0055148
URL : https://hal.archives-ouvertes.fr/hal-00544505

D. Nowak, Spécification et preuve de systèmes réactifs, 1999.

J. Palsberg, A provably correct compiler generator, Proc. ESOP'92, pp.418-434, 1992.
DOI : 10.1007/3-540-55253-7_25

J. Paris, Exécution de tâches asynchrones depuis Esterel, 1992.

G. Plotkin, A structural approach to operational semantics, 1981.

M. Poigné, O. Morley, L. Maffe¨?smaffe¨?s, R. Holenderski, and . Budde, The synchronous approach to designing reactive systems, Formal Methods in System Design, vol.12, issue.2, pp.163-187, 1998.
DOI : 10.1023/A:1008697810328

W. Polak, Compiler Specification and Verification [Pot02] Dumitru Potop-Butucaru. Optimizations for Faster Execution of Esterel Programs, 1981.

A. Pnueli, M. Siegel, and E. Singerman, Translation validation, Proc. TACAS'98, pp.151-166
DOI : 10.1007/BFb0054170

A. Pnueli, O. Strichman, and M. Siegel, The Code Validation Tool (CVT), International Journal on Software Tools for Technology Transfer (STTT), vol.2, issue.2, pp.192-201, 1998.
DOI : 10.1007/s100090050027

A. Pnueli, O. Strichman, and M. Siegel, Translation Validation: From SIGNAL to C, Correct System Design, Recent Insight and Advances, pp.231-255, 1999.
DOI : 10.1007/3-540-48092-7_11

[. Schneider, J. Brandt, and T. Schüle, A Verified Compiler for Synchronous Programs with Local Declarations, Proc. SLAP'04, 2004.
DOI : 10.1016/j.entcs.2006.02.028

K. Schneider, Embedding imperative synchronous languages in interactive theorem provers, Proceedings Second International Conference on Application of Concurrency to System Design, p.143, 2001.
DOI : 10.1109/CSD.2001.981772

. Sr98-]-bran, J. Selic, and . Rumbaugh, Using UML for modeling complex real-time systems, 1998.

E. M. Sentovich, H. Toma, and G. Berry, Latch optimization in circuits generated from high-level descriptions, Proceedings of International Conference on Computer Aided Design, pp.428-435, 1996.
DOI : 10.1109/ICCAD.1996.569833
URL : https://hal.archives-ouvertes.fr/inria-00073756

S. Stepney, High Integrity Compilation: A Case Study, 1993.

R. Neil and . Storey, Safety-Critical Computer Systems, 1996.

K. Schneider and M. Wenz, A new method for compiling schizophrenic synchronous programs, Proceedings of the international conference on Compilers, architecture, and synthesis for embedded systems , CASES '01, pp.49-58, 2001.
DOI : 10.1145/502217.502226

[. Tanzi, Traduction Structurelle des Programmes Esterel en Automates, 1985.

O. Tardieu, A Deterministic Logical Semantics for Esterel, Proc. SOS Work- shop'04, 2004.
DOI : 10.1016/j.entcs.2004.09.040

O. Tardieu, Goto and Concurrency Introducing Safe Jumps in Esterel, Proc. SLAP'04, 2004.
DOI : 10.1016/j.entcs.2006.02.025

O. Tardieu, R. De, and S. , Instantaneous Termination in Pure Esterel, Proc. SAS'03, pp.91-108, 2003.
DOI : 10.1007/3-540-44898-5_6

O. Tardieu, R. De, and S. , Curing Schizophrenia by program rewriting in Esterel, Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2004. MEMOCODE '04., 2004.
DOI : 10.1109/MEMCOD.2004.1459813

D. Terrasse, A first step towards the proof of correctness of the v5 Esterel compiler in Coq, 2000.