D. Biernacki, J. Colaço, G. Hamon, and M. Pouzet, Clock-directed modular code generation for synchronous data-flow languages, Proceedings of the 9th ACM SIGPLAN Conference on Languages, Compilers, and Tools for Embedded Systems, pp.121-130, 2008.

S. Blazy, Z. Dargaye, and X. Leroy, Formal Verification of a C Compiler Front-End, Proceedings of the 14th International Symposium on Formal Methods, pp.460-475, 2006.
DOI : 10.1007/11813040_31
URL : https://hal.archives-ouvertes.fr/inria-00106401

T. Bourke, L. Brun, P. Dagand, X. Leroy, M. Pouzet et al., A Formally Verified Compiler for Lustre, Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.586-601, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01512286

P. Caspi, D. Pilaud, N. Halbwachs, and J. A. Plaice, LUSTRE: A declarative language for programming synchronous systems, Proceedings of the 14th ACM SIGPLAN-SIGACT Symposium on Principles Of Programming Languages, pp.178-188, 1987.

J. Colaço, B. Pagano, and M. Pouzet, A conservative extension of synchronous data-flow with state machines, Proceedings of the 5th ACM international conference on Embedded software , EMSOFT '05, 2005.
DOI : 10.1145/1086228.1086261

G. Hamon and M. Pouzet, Modular resetting of synchronous data-flow programs, Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming , PPDP '00, pp.289-300, 2000.
DOI : 10.1145/351268.351300
URL : https://hal.archives-ouvertes.fr/hal-01573195

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

, The Coq Development Team. 2016. The Coq proof assistant reference manual