P. Audebaud and C. Paulin-mohring, Proofs of randomized algorithms in Coq, Mathematics of Program Construction, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00431771

P. Audebaud and C. Paulin-mohring, Proofs of randomized algorithms in Coq, Science of Computer Programming, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00431771

Y. Bertot, Filters on CoInductive Streams, an Application to Eratosthenes??? Sieve, International Conference of Typed Lambda Calculi and Applications, pp.102-115, 2005.
DOI : 10.1007/11417170_9

URL : https://hal.archives-ouvertes.fr/inria-00070658

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, 2004.
DOI : 10.1007/978-3-662-07964-5

URL : https://hal.archives-ouvertes.fr/hal-00344237

S. Boulmé and G. Hamon, Certifying Synchrony for Free Short version of A clocked denotational semantics for Lucid-Synchrone in Coq, International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), 2001.

V. Capretta, General recursion via coinductive types, Logical Methods in Computer Science, vol.1, issue.2, pp.1-28, 2005.
DOI : 10.2168/LMCS-1(2:1)2005

URL : http://arxiv.org/abs/cs/0505037

P. Caspi and M. Pouzet, Synchronous Kahn Networks, ACM SIG- PLAN International Conference on Functional Programming, 1996.

A. Cohen, M. Duranton, C. Eisenbeis, C. Pagetti, F. Plateau et al., N -Synchronous Kahn Networks: a Relaxed Model of Synchrony for Real-Time Systems, ACM International Conference on Principles of Programming Languages (POPL'06), 2006.

B. Courcelle, G. Kahn, and J. Vuillemin, Algorithmes d'´ equivalence et de réductionréductionà des expressions minimales dans une classe d'´ equations récursives simples, Automata, Languages and Programming, pp.200-213, 1974.

N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, The synchronous dataflow programming language lustre, Proceedings of the IEEE, pp.1305-1320, 1991.

G. Kahn, The semantics of a simple language for parallel programming, Information Processing, 1974.

G. Kahn and D. Macqueen, Coroutines and networks of parallel processes, Information Processing, 1977.
URL : https://hal.archives-ouvertes.fr/inria-00306565

G. Kahn and G. D. Plotkin, Concrete domains, Theoretical Computer Science, vol.121, issue.1-2, pp.187-277, 1993.
DOI : 10.1016/0304-3975(93)90090-G

D. Pilaud, P. Caspi, N. Halbwachs, and J. Plaice, Lustre: a declarative language for programming synchronous systems, 14th ACM Conference on Principles of Programming Languages, pp.178-188, 1987.