S. V. Adve and K. Gharachorloo, Shared memory consistency models: a tutorial, Computer, vol.29, issue.12, pp.66-76, 1995.
DOI : 10.1109/2.546611

J. Alglave, A Shared Memory Poetics, 2010.

J. Alglave, D. Longuet, and L. Maranget, Testing for Weak Memory Model Exploration

J. Alglave and L. Maranget, Stability in Weak Memory Models, CAV, 2011.
DOI : 10.1007/978-3-540-30482-1_11
URL : https://hal.archives-ouvertes.fr/hal-01100806

J. Alglave, L. Maranget, S. Sarkar, and P. Sewell, Fences in Weak Memory Models, 2010.
DOI : 10.1007/978-3-642-14295-6_25
URL : https://hal.archives-ouvertes.fr/hal-01100859

Y. Bertot and P. Casteran, Coq'Art, EATCS Texts in Theoretical Computer Science
URL : https://hal.archives-ouvertes.fr/hal-00344237

F. Blanqui and A. Koprowski, CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates, Mathematical Structures in Computer Science, vol.37, issue.04
DOI : 10.1016/S0890-5401(03)00011-7
URL : https://hal.archives-ouvertes.fr/inria-00543157

S. Burckhardt and M. Musuvathi, Memory Model Safety of Programs, 2008.

A. Fox, M. Gordon, and M. Myreen, Specification and Verification of ARM Hardware and Software, Design and Verification of Microprocessor Systems for High- Assurance Applications, 2010.
DOI : 10.1007/978-1-4419-1539-9_8

A. Fox and M. Myreen, A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture, 2010.
DOI : 10.1007/978-3-642-14052-5_18

G. Gonthier and A. Mahboubi, An introduction to small scale reflection in Coq, Journal of Formalized Reasoning, vol.3, pp.95-152, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00515548

G. Gonthier, A. Mahboubi, and E. Tassi, A small scale reflection extension for the Coq system
URL : https://hal.archives-ouvertes.fr/inria-00258384

L. Lamport, How to make a correct multiprocess program execute correctly on a multiprocessor, IEEE Transactions on Computers, vol.46, issue.7, pp.779-782, 1979.
DOI : 10.1109/12.599898

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

J. Manson, W. Pugh, and S. V. Adve, The Java Memory Model, POPL, 2005.
DOI : 10.1145/1047659.1040336

M. Myreen and M. Gordon, Verified LISP Implementations on ARM,??x86??and??PowerPC, TPHOL 09
DOI : 10.1007/978-3-540-71067-7_6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.154.5045

S. Owens, Reasoning about the Implementation of Concurrency Abstractions on x86-TSO, 2010.
DOI : 10.1007/978-3-642-14107-2_23

S. Owens, S. Sarkar, and P. Sewell, A Better x86 Memory Model, p.86, 2009.

S. and L. Roux, Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence, TPHOLs, 2009.

S. Sarkar, P. Sewell, F. Zappa-nardelli, S. Owens, T. Ridge et al., The Semantics of x86-CC Multiprocessor Machine Code, POPL, 2009.

J. Sevcik, V. Vafeiadis, F. Zappa-nardelli, P. Sewell, and S. Jagannathan, Relaxedmemory concurrency and verified compilation, POPL, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00907801