D. Cachera, T. Jensen, D. Pichardie, and V. Rusu, Extracting a Data Flow Analyser in Constructive Logic, 13th European Symposium on Programming, pp.385-400, 2004.
DOI : 10.1007/978-3-540-24725-8_27
URL : https://hal.archives-ouvertes.fr/inria-00564633

G. Klein and T. Nipkow, Verified bytecode verifiers, Theoretical Computer Science, vol.298, issue.3, pp.583-626, 2002.
DOI : 10.1016/S0304-3975(02)00869-1

S. Lerner, T. Millstein, E. Rice, and C. Chambers, Automated soundness proofs for dataflow analyses and transformations via local rules, 32nd symposium on Principles of Programming Languages, pp.364-377, 2005.
DOI : 10.1145/1040305.1040335
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.115.9525

G. Morrisett, D. Walker, K. Crary, and N. Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems, vol.21, issue.3, pp.528-569, 1999.

G. C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.106-119, 1997.
DOI : 10.1145/263699.263712

A. Pnueli, M. Siegel, and E. Singerman, Translation validation, TACAS '98, pp.151-166, 1998.
DOI : 10.1007/BFb0054170

M. Rinard, Credible compilation, 1999.