S. Blazy and X. Leroy, Mechanized Semantics for the Clight Subset of the C Language, Journal of Automated Reasoning, vol.29, issue.6, pp.263-288, 2009.
DOI : 10.1007/s10817-009-9148-3

URL : https://hal.archives-ouvertes.fr/inria-00352524

J. Chen, A typed intermediate language for compiling multiple inheritance, 34th symp. Principles of Programming Languages, pp.25-30, 2007.

B. Dawes and I. Wg21, POD's Revisited; Resolving Core Issue 568 (Revision 2) URL http://www.open-std, 2007.

M. A. Ellis and B. Stroustrup, The Annotated C++ Reference Manual, 1990.

J. Gil and P. F. Sweeney, Space and time-efficient memory layout for multiple inheritance, 14th conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 1999), pp.256-275, 1999.

J. Y. Gil, W. Pugh, G. E. Weddell, and Y. Zibin, Two-dimensional bidirectional object layout, ACM Transactions on Programming Languages and Systems, vol.30, issue.5, pp.1-38, 2008.
DOI : 10.1145/1387673.1387677

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

G. Klein and T. Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Transactions on Programming Languages and Systems, vol.28, issue.4, pp.619-695, 2006.
DOI : 10.1145/1146809.1146811

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

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814

URL : https://hal.archives-ouvertes.fr/inria-00415861

C. Luo and S. Qin, Separation Logic for Multiple Inheritance, Electronic Notes in Theoretical Computer Science, vol.212, pp.27-40, 2008.
DOI : 10.1016/j.entcs.2008.04.051

N. Myers, The empty member C++ optimization. Dr Dobb's Journal, 1997.

G. Ramalingam and H. Srinivasan, A member lookup algorithm for C++, Programming Language Design and Implementation (PLDI'97), pp.18-30, 1997.

T. Ramananandro, Formal verification of object layout for C++ multiple inheritance ? Coq development and supplementary material, 2010.

J. G. Rossie and D. P. Friedman, An algebraic semantics of subobjects, 10th conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 1995), pp.187-199, 1995.

P. F. Sweeney and M. G. Burke, Quantifying and evaluating the space overhead for alternative C++ memory layouts. Software: Practice and Experience, pp.595-636, 2003.

H. Tuch, Formal Verification of C Systems Code, Journal of Automated Reasoning, vol.5, issue.3, pp.125-187, 2009.
DOI : 10.1007/s10817-009-9120-2

D. Wasserrab, T. Nipkow, G. Snelting, and F. Tip, An operational semantics and type safety proof for multiple inheritance in C++, 21st conf. on Object-Oriented Programming, Systems, Languages, and Applications, pp.345-362, 2006.