A. Ahmed, Semantics of types for mutable state, 2004.

A. Ahmed, D. Dreyer, and A. Rossberg, State-dependent representation independence, Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009.

A. Appel, Foundational proof-carrying code, Proc. 16th IEEE Symposium on Logic in Computer Science (LICS), 2001.

A. Appel and D. Mcallester, An indexed model of recursive types for foundational proof-carrying code, ACM Transactions on Programming Languages and Systems, vol.23, issue.5, 2001.
DOI : 10.1145/504709.504712

A. W. Appel, P. Mellì-es, C. D. Richards, and J. Vouillon, A very modal model of a modern, major, general type system, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.109-122, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00150978

N. Benton, Abstracting Allocation, CSL '06, 2006.
DOI : 10.1007/11874683_12

N. Benton and B. Leperchey, Relational Reasoning in a Nominal Semantics for Storage, Proc. 7th International Conference on Typed Lambda Calculi and Applications (TLCA), 2005.
DOI : 10.1007/11417170_8
URL : https://hal.archives-ouvertes.fr/hal-00102772

N. Benton and C. Hur, Biorthogonality, step-indexing and compiler correctness, ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming, pp.97-108, 2009.

N. Benton and N. Tabareau, Compiling functional types to relational specifications for low level imperative code, Proceedings of the 4th international workshop on Types in language design and implementation, TLDI '09, pp.3-14, 2009.
DOI : 10.1145/1481861.1481864
URL : https://hal.archives-ouvertes.fr/hal-00341404

M. Dave, Compiler verification, ACM SIGSOFT Software Engineering Notes, vol.28, issue.6, 2003.
DOI : 10.1145/966221.966235

J. Krivine, Realizability in classical logic Course notes of a series of lectures given in the University of Marseille, may 2004 (last revision: july 2005) Panoramas et syntheses

X. Leroy, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, Proc. 33rd Symposium on Principles of Programming Languages (POPL), 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

J. Mccarthy and J. Painter, Correctness of a compiler for arithmetic expressions, Proceedings Symposium in Applied Mathematics, pp.33-41, 1967.
DOI : 10.1090/psapm/019/0242403

Z. Ni and Z. Shao, Certified assembly programming with embedded code pointers, Proc. 33rd ACM Symposium on Principles of Programming Languages (POPL), 2006.

A. M. Pitts and I. D. Stark, Operational reasoning for functions with local state, Higher Order Operational Techniques in Semantics. CUP, 1998.

G. Tan, A. Appel, K. Swadi, and D. Wu, Construction of a Semantic Model for a Typed Assembly Language, Proc. 5th Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2004.
DOI : 10.1007/978-3-540-24622-0_4

D. Yu, N. A. Hamid, and Z. Shao, Building certified libraries for PCC: Dynamic storage allocation, Science of Computer Programming, vol.50, 2004.