This page contains the Coq development accompanying the following article:
Xavier Leroy and Sandrine Blazy, Formal verification of a C-like memory model and its uses for verifying program transformations, 2007. Submitted for publication.
Copyright 2006, 2007 Institut National de Recherche en Informatique et Automatique (INRIA). These files are distributed under the terms of the GNU Public License version 2.