A. W. Appel, Foundational proof-carrying code, IEEE Symp. on Logic in Computer Science (LICS), p.247, 2001.
DOI : 10.1109/fits.2003.1264926

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

A. Sampaio, An algebraic approach to compiler design, volume 4 of AMAST series in computing, World Scientic, 1997.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

R. Bornat, Proving Pointer Programs in Hoare Logic, 5th Conf. on Mathematics of Program Construction, p.102126, 2000.
DOI : 10.1007/10722010_8

D. Cachera, T. Jensen, D. Pichardie, and V. Rusu, Extracting a Data Flow Analyser in Constructive Logic, Proc. of Europ. Symp. on Programming number 2986 in Lecture Notes in Computer Science, p.385400, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00564633

J. Chrz¡szcz, Modules in Type Theory with Generative Denitions, 2004.

D. Yu and Z. Shao, Verication of safety properties for concurrent assembly code, Int. Conf. on Functional Programming (ICFP), p.175188, 2004.

J. Filliâtre and C. Marché, Multi-Prover Verication of C Programs, 6th Int

G. Goos and W. Zimmermann, Verication of compilers, Correct System Design, Recent Insight and Advances, p.201230, 1999.

G. Watson, Compilation of renement for a practical language, 5th Int. Conf. on Formal Engineering Methods (ICFEM), 2003.

N. Hamid, Z. Shao, V. Trifonov, S. Monnier, and Z. Ni, A syntactic approach to foundational proof-carrying code, Journal of Automated Reasoning, pp.31-34, 2003.

X. Leroy, Formal certication of a compiler back-end, or: programming a compiler with a proof assistant, 2005.

P. Letouzey, Programmation fonctionnelle certiée L'extraction de programmes dans l'assistant Coq, 2004.

F. Mehta and T. Nipkow, Proving pointer programs in higher-order logic, Automated Deduction (CADE-19), volume 2741 of Lecture Notes in Computer Science, p.121135, 2003.

I. Mijajlovic and N. Torp-smith, Renement in separation context. In Second workshop on semantics, program anlysis and computing analysis for memory management (SPACE), 2004.

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

G. Necula, Translation validation for an optimizing compiler, ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), pp.83-95, 2000.

A. Pnueli, M. Siegel, and E. Singerman, Translation validation, Proc. of the 4th Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems (TACAS), p.151166, 1998.
DOI : 10.1007/BFb0054170

M. Rinard and D. Marinov, Credible compilation with pointers, Workshop on Run-Time Result Verication (RTRV), 1999.

X. Shen, A. , and L. Rudolph, Commit-reconcile & fences (CRF), ISCA '99: 26th symposium on Computer architecture, p.150161, 1999.
DOI : 10.1145/307338.300992

S. Lerner, T. Millstein, E. Rice, and C. Chambers, Automated soundness proofs for dataow analyses and transformations, Principles Of Progamming Languages Conf. (POPL), 2005.

S. Monnier, Typed regions In workshop on semantics, program anlysis and computing analysis for memory management (SPACE), 2004.

R. D. Tennent and D. R. Ghica, Abstract models of storage. Higher-Order and Symbolic Computation, p.119129, 2000.

D. Walker, Stacks, heaps and regions: one logic to bind them In Second workshop on semantics, program anlysis and computing analysis for memory management (SPACE), 2004.

Y. Hu, C. Barrett, B. Goldberg, and A. Pnueli, Validating More Loop Optimizations, Workshop on Compiler Optimization Meets Compiler Verication (COCV), 2005.
DOI : 10.1016/j.entcs.2005.02.044