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

S. Blazy and X. Leroy, Mechanized semantics for the Clight subset of the C language, J. Automated Reasoning, vol.43, issue.3, pp.263-288, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00352524

S. Boulmé and G. Hamon, Certifying synchrony for free, R. Nieuwenhuis et A. Voronkov, éds : Proc. 8th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001), vol.2250, pp.495-506, 2001.

S. Boulmé and G. Hamon, A clocked denotational semantics for Lucid-Synchrone in Coq, Rap. tech, vol.6, 2001.

T. Bourke, L. Brun, P. Dagand, X. Leroy, M. Pouzet et al., A formally verified compiler for Lustre, Proc. 2017 ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), pp.586-601, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01512286

T. Bourke, P. Dagand, M. Pouzet, and L. Rieg, Vérification de la génération modulaire du code impératif pour Lustre, J. Signoles et S. Boldo, éds : 28 ièmes Journées Francophones des Langages Applicatifs, pp.165-179, 2017.

P. Caspi, Clocks in dataflow languages, Theor. Comp. Sci, vol.94, issue.1, pp.125-140, 1992.

J. Colaço, Private communication, 2017.

J. Colaço, B. Pagano, and M. Pouzet, Scade 6 : A formal language for embedded critical software development, Proc. 11th Int. Symp. Theoretical Aspects of Software Engineering (TASE 2017), 2017.

J. Colaço and M. Pouzet, Clocks as first class abstract types, R. Alur et I. Lee, éds : Proc. 3rd Int. Conf. on Embedded Software (EMSOFT 2003), pp.134-155, 2003.

N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, The synchronous dataflow programming language LUSTRE. Proc. IEEE, vol.79, pp.1305-1320, 1991.

-. C. Programming-languages, . Standard, . Iec, . Geneva, and . Switzerland, , 1999.

R. Kumar, M. O. Myreen, M. Norrish, and S. Owens, CakeML : A verified implementation of ML, Proc. 41st ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, pp.179-191, 2014.

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

, The Coq Development Team : The Coq proof assistant reference manual