This directory contains the HOL4 proof of the equivalence of the SC-total and SC-partial representations of the C11 memory model. To read the statement of the proof, refer to cpp11soundness.lem. It requires Lem, Herd and HOL, which must be pointed to in ./Makefile by specifying LEMDIR, HERDDIR and HOLDIR. In addition, Lem's HOL library must be pointed to by specifying HOLHEAP in ./Holmakefile.

After setting up the makefiles, to run the proofs type "make". They take some time (over 10 minutes on a 2.13GHz Core 2 Duo with 4GB of RAM).

