A. W. Appel, Tactics for separation logic, 2006.

W. Andrew, S. Appel, and . Blazy, Separation logic for small-step Cminor (extended version), 2007.

S. Blazy, Z. Dargaye, and X. Leroy, Formal Verification of a C Compiler Front-End, Symp. on Formal Methods (FM'06), pp.460-475, 2006.
DOI : 10.1007/11813040_31
URL : https://hal.archives-ouvertes.fr/inria-00106401

S. Blazy and X. Leroy, Formal Verification of a Memory Model for C-Like Imperative Languages, Formal Engineering Methods, pp.280-299, 2005.
DOI : 10.1007/11576280_20
URL : https://hal.archives-ouvertes.fr/inria-00077921

R. Bornat, C. Calcagno, O. Peter, M. Hearn, and . Parkinson, Permission accounting in separation logic, POPL '05, pp.259-270, 2005.

Z. Dargaye, Décurryfication certifiée, JFLA (Journées Françaises des Langages Applicatifs), pp.119-133, 2007.

S. Ishtiaq, O. Peter, and . Hearn, BI as an assertion language for mutable data structures, POPL'01, pp.14-26, 2001.

G. Klein, H. Tuch, and M. Norrish, Types, bytes, and separation logic, POPL'07, pp.97-108, 2007.

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), 2005.
DOI : 10.1109/SEFM.2005.51

X. Leroy, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, POPL'06, pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

J. Strother and M. , A mechanically verified language implementation, Journal of Automated Reasoning, vol.5, issue.4, pp.461-492, 1989.

Z. Ni and Z. Shao, Certified assembly programming with embedded code pointers, POPL'06, pp.320-333, 2006.

O. Peter, J. Hearn, H. Reynolds, and . Yang, Local reasoning about programs that alter data structures, CSL'01, pp.1-19, 2001.

M. J. Parkinson, Local Reasoning for Java, 2005.

N. Schirmer, Verification of Sequential Imperative Programs in Isabelle, 2006.