A. W. Appel, Modern Compiler Implementation in ML, 1998.
DOI : 10.1017/CBO9780511811449

C. W. Barret, Y. Fang, B. Goldberg, Y. Hu, A. Pnueli et al., TVOC: A Translation Validator for Optimizing Compilers, Computer Aided Verification, 17th Int. Conf., CAV 2005, pp.291-295, 2005.
DOI : 10.1007/11513988_29

G. Barthe, J. Forest, D. Pichardie, and V. Rusu, Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant, Functional and Logic Programming, 8th Int. Symp., FLOPS 2006, pp.114-129, 2006.
DOI : 10.1007/11737414_9
URL : https://hal.archives-ouvertes.fr/inria-00564237

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

D. Cachera, T. Jensen, D. Pichardie, and V. Rusu, Extracting a data flow analyser in constructive logic, Theoretical Computer Science, vol.342, issue.1, pp.56-78, 2005.
DOI : 10.1016/j.tcs.2005.06.004
URL : https://hal.archives-ouvertes.fr/inria-00564633

A. Maulik and . Dave, Compiler verification: a bibliography, SIGSOFT Softw. Eng. Notes, vol.28, issue.6, pp.2-2, 2003.

J. R. Ellis, Bulldog: a compiler for VLSI architectures ACM Doctoral Dissertation Awards, 1986.

B. Goldberg, L. Zuck, and C. Barret, Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers, Proc. Workshop Compiler Optimization Meets Compiler Verification, pp.53-71, 2004.
DOI : 10.1016/j.entcs.2005.01.030

Y. Huang, B. R. Childers, and M. L. Soffa, Catching and Identifying Bugs in Register Allocation, Static Analysis, 13th Int. Symp., SAS 2006, pp.281-300, 2006.
DOI : 10.1007/11823230_19

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

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, pp.619-695, 2006.
DOI : 10.1145/1146809.1146811

D. Leinenbach, W. Paul, and E. Petrova, Towards the formal verification of a C0 compiler: code generation and implementation correctness, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), pp.2-11, 2005.
DOI : 10.1109/SEFM.2005.51

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

X. Leroy, The Compcert certified compiler back-end

R. Leviathan and A. Pnueli, Validating software pipelining optimizations, Proceedings of the international conference on Compilers, architecture, and synthesis for embedded systems , CASES '02, pp.280-287, 2002.
DOI : 10.1145/581630.581676

S. Steven and . Muchnick, Advanced compiler design and implementation, 1997.

C. George and . Necula, Translation validation for an optimizing compiler, Programming Language Design and Implementation, pp.83-95, 2000.

A. Pnueli, O. Shtrichman, and M. Siegel, The Code Validation Tool (CVT), International Journal on Software Tools for Technology Transfer (STTT), vol.2, issue.2, pp.192-201, 1998.
DOI : 10.1007/s100090050027

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

X. Rival, Symbolic transfer function-based approaches to certified compilation, 31st symposium Principles of Programming Languages, pp.1-13, 2004.

B. N. Emin-gün-sirer and . Bershad, Testing Java virtual machines, Proc. Int. Conf. on Software Testing And Review, 1999.

M. Strecker, Compiler verification for C0, 2005.

L. Zuck, A. Pnueli, and R. Leviathan, Validation of optimizing compilers, 2001.

L. Zuck, A. Pnueli, Y. Fang, and B. Goldberg, VOC, Electronic Notes in Theoretical Computer Science, vol.65, issue.2, pp.223-247, 2003.
DOI : 10.1016/S1571-0661(04)80393-1