M. S. Ager, O. Danvy, and J. Midtgaard, A functional correspondence between monadic evaluators and abstract machines for languages with computational effects, Theoretical Computer Science, vol.342, issue.1, pp.149-172, 2005.
DOI : 10.1016/j.tcs.2005.06.008

A. Appel, Foundational proof-carrying code, Proc. 16th IEEE Symposium on Logic in Computer Science (LICS), 2001.
DOI : 10.1109/lics.2001.932501

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

A. Appel and D. Mcallester, An indexed model of recursive types for foundational proofcarrying code, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.23, issue.5, 2001.

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 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.
DOI : 10.1145/1596550.1596567

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

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

P. Landin, The Mechanical Evaluation of Expressions, The Computer Journal, vol.6, issue.4, p.308, 1964.
DOI : 10.1093/comjnl/6.4.308

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

A. Nanevski, G. Morrisett, and L. Birkedal, Polymorphism and separation in hoare type theory, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, p.73, 2006.

J. Van-oosten, Realizability: a historical essay, Mathematical Structures in Computer Science, vol.12, issue.03, pp.239-263, 2002.
DOI : 10.1017/S0960129502003626