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
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
An indexed model of recursive types for foundational proofcarrying code, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.23, issue.5, 2001. ,
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
Abstracting Allocation, CSL '06, 2006. ,
DOI : 10.1007/11874683_12
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
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
Compiler verification, ACM SIGSOFT Software Engineering Notes, vol.28, issue.6, 2003. ,
DOI : 10.1145/966221.966235
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 ,
The Mechanical Evaluation of Expressions, The Computer Journal, vol.6, issue.4, p.308, 1964. ,
DOI : 10.1093/comjnl/6.4.308
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
Correctness of a compiler for arithmetic expressions, Proceedings Symposium in Applied Mathematics, pp.33-41, 1967. ,
DOI : 10.1090/psapm/019/0242403
Polymorphism and separation in hoare type theory, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, p.73, 2006. ,
Realizability: a historical essay, Mathematical Structures in Computer Science, vol.12, issue.03, pp.239-263, 2002. ,
DOI : 10.1017/S0960129502003626