C. Auger, J. Colaço, and G. Hamon, Pouzet : A formalization and proof of a modular Lustre code generator. En préparation, 2016.

D. Biernacki, J. Colaço, and G. Hamon, Pouzet : Clock-directed modular code generation for synchronous data-flow languages, LCTES'08, pp.121-130, 2008.
DOI : 10.1145/1379023.1375674

S. Blazy, Z. Dargaye, and X. Leroy, Formal Verification of a C Compiler Front-End, FM'06 de Lecture Notes in Comp. Sci, pp.460-475, 2006.
DOI : 10.1007/11813040_31
URL : https://hal.archives-ouvertes.fr/inria-00106401

S. Boulmé and G. Hamon, Certifying Synchrony for Free, LPAR'01 de Lecture Notes in Comp. Sci, pp.495-506, 2001.
DOI : 10.1007/3-540-45653-8_34

P. Caspi, A. Curic, A. Maignan, C. Sofronis, and S. Tripakis, Niebert : From Simulink to SCADE/Lustre to TTA : a layered approach for distributed embedded applications, LCTES'03, pp.153-162, 2003.
DOI : 10.1145/780732.780754

P. Caspi, D. Pilaud, and N. Halbwachs, Plaice : LUSTRE : A declarative language for programming synchronous systems, POPL'87, pp.178-188, 1987.

J. Colaço and B. Pagano, Pouzet : A conservative extension of synchronous data-flow with state machines, EMSOFT'05, pp.173-182, 2005.

S. Coupet-grimal and L. Jakubiec, Hardware Verification Using Co-induction in COQ, TPHOLs'99 1690 de Lecture Notes in Comp. Sci, pp.91-108, 1999.
DOI : 10.1007/3-540-48256-3_7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.6015

A. Dieumegard, P. Garoche, T. Kahsai, A. Taillar, and X. Thirioux, Compilation of synchronous observers as code contracts, Proceedings of the 30th Annual ACM Symposium on Applied Computing, SAC '15, pp.1933-1939, 2015.
DOI : 10.1145/2695664.2695819

L. Gérard, A. Guatto, and C. Pasteur, Pouzet : A modular memory optimization for synchronous data-flow languages : application to arrays in a Lustre compiler, LCTES'12, pp.51-60, 2012.

E. Gimenez, E. Ledinot, G. Ii, S. Verilog, and J. , Certification de SCADE V3, 2000.

G. Hagen and C. , Tinelli : Scaling up the formal verification of Lustre programs with SMT-based techniques, FMCAD'08, p.15, 2008.

N. Halbwachs, F. Lagnier, and C. , 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

G. Hamon, Pouzet : Modular resetting of synchronous data-flow programs, PPDP'00, pp.289-300, 2000.
DOI : 10.1145/351268.351300
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.23.8670

N. Izerrouken, X. Thirioux, M. Pantel, and M. Strecker, Certifying an automated code generator using formal tools : Preliminary experiments in the GeneAuto project, ERTS'08. Société des Ingénieurs de l'Automobile, 2008.

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861

V. Ngo, J. Talpin, T. Gautier, L. Besnard, and P. L. Guernic, Modular translation validation of a full-sized synchronous compiler using off-the-shelf verification tools, Proceedings of the 18th International Workshop on Software and Compilers for Embedded Systems, SCOPES '15
DOI : 10.1145/2764967.2775291
URL : https://hal.archives-ouvertes.fr/hal-01148919

C. Paulin-mohring, A constructive denotational semantics for Kahn networks in Coq, From Semantics to Computer Science : Essays in Honour of Gilles Kahn, pp.383-413, 2009.
DOI : 10.1017/CBO9780511770524.018
URL : https://hal.archives-ouvertes.fr/inria-00431806

A. Pnueli, M. Siegel, and O. Shtrichman, Translation validation for synchronous languages, ICALP'98 1443 de Lecture Notes in Comp. Sci, pp.235-246, 1998.
DOI : 10.1007/BFb0055057

M. Pouzet, Lucid Synchrone, version 3. Tutorial and reference manual, 2006.

M. Ryabtsev and O. Strichman, Translation Validation: From Simulink to C, CAV'09 de Lecture Notes in Comp. Sci, pp.696-701, 2009.
DOI : 10.1007/978-3-642-02658-4_57
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.172.9992

K. Schneider, Embedding imperative synchronous languages in interactive theorem provers, Proceedings Second International Conference on Application of Concurrency to System Design, pp.143-154, 2001.
DOI : 10.1109/CSD.2001.981772
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.559.7027