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. ,
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
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. ,
A clocked denotational semantics for Lucid-Synchrone in Coq, Rap. tech, vol.6, 2001. ,
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
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. ,
Clocks in dataflow languages, Theor. Comp. Sci, vol.94, issue.1, pp.125-140, 1992. ,
Private communication, 2017. ,
Scade 6 : A formal language for embedded critical software development, Proc. 11th Int. Symp. Theoretical Aspects of Software Engineering (TASE 2017), 2017. ,
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. ,
, The synchronous dataflow programming language LUSTRE. Proc. IEEE, vol.79, pp.1305-1320, 1991.
, , 1999.
CakeML : A verified implementation of ML, Proc. 41st ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, pp.179-191, 2014. ,
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