A. Berarducci and M. Dezani-ciancaglini, Infinite ??-calculus and types, Theoretical Computer Science, vol.212, issue.1-2, pp.29-75, 1999.
DOI : 10.1016/S0304-3975(98)00135-2
URL : http://doi.org/10.1016/s0304-3975(98)00135-2

Y. Bertot, Filters on CoInductive Streams, an Application to Eratosthenes??? Sieve, Typed Lambda Calculi and Applications (TLCA'05), 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 ? Coq'Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

P. Cousot and R. Cousot, Inductive definitions, semantics and abstract interpretations, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '92, pp.83-94, 1992.
DOI : 10.1145/143165.143184

V. Gapeyev, M. Levin, and B. Pierce, Recursive subtyping revealed, J. Func. Progr, vol.12, issue.6, pp.511-548, 2003.
DOI : 10.1145/357766.351261
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.4619

E. Giménez, Codifying guarded definitions with recursive schemes, Types for Proofs and Programs. International Workshop TYPES '94, pp.39-59, 1994.
DOI : 10.1007/3-540-60579-7_3

B. Grégoire, Compilation des termes de preuves: un (nouveau) mariage entre Coq et OCaml, 2003.

C. A. Gunter and D. Rémy, A proof-theoretic assessment of runtime type errors, 1993.

T. Hardin, L. Maranget, and B. Pagano, Functional runtime systems within the lambda-sigma calculus, Journal of Functional Programming, vol.8, issue.2, pp.131-176, 1998.
DOI : 10.1017/S0956796898002986
URL : https://hal.archives-ouvertes.fr/hal-01199543

R. Kennaway, J. W. Klop, M. R. Sleep, and F. Vries, Infinitary lambda calculus, Theoretical Computer Science, vol.175, issue.1, pp.93-125, 1997.
DOI : 10.1016/S0304-3975(96)00171-5
URL : http://doi.org/10.1016/s0304-3975(96)00171-5

G. Klein and T. Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Transactions on Programming Languages and Systems, vol.28, issue.4, 2004.
DOI : 10.1145/1146809.1146811

X. Leroy, Coinductive big-step operational semantics ? the Coq development. Available from pauillac.inria.fr/~xleroy, 2005.

X. Leroy, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, 33rd symp. Principles of Progr. Lang, pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

X. Leroy and F. Rouaix, Security properties of typed applets, Secure Internet Programming ? Security issues for Mobile and Distributed Objects, pp.147-182, 1999.
DOI : 10.1007/3-540-48749-2_7
URL : https://hal.archives-ouvertes.fr/hal-01499957

R. Milner and M. Tofte, Co-induction in relational semantics, Theoretical Computer Science, vol.87, issue.1, pp.209-220, 1991.
DOI : 10.1016/0304-3975(91)90033-X
URL : http://doi.org/10.1016/0304-3975(91)90033-x

M. Rittri, Proving the correctness of a virtual machine by a bisimulation, 1988.

A. Stoughton, An Operational Semantics Framework Supporting the Incremental Construction of Derivation Trees, Second Workshop on Higher-Order Operational Techniques in Semantics (HOOTS II), 1998.
DOI : 10.1016/S1571-0661(05)80693-0

M. Strecker, Compiler verification for C0, 2005.

A. K. Wright and M. Felleisen, A Syntactic Approach to Type Soundness, Information and Computation, vol.115, issue.1, pp.38-94, 1994.
DOI : 10.1006/inco.1994.1093