Formal proof development for the AxSL logic

This artifact is a mechanised proof development that contains formalised definitions and proofs that can be checked by the Coq proof assistant. It contains all the results presented in the paper.

The project can be compiled using the OCaml building system dune with required denpendencies installed. The building scripts are organised into dune-project and severnal dune files.

Refer to INSTALL.md for more information on building it in a Docker environment or manually.

The Coq development is organised into two subdirectories.

The theories directory contains the primary Coq development of the work. The system-semantics directory contains the Coq infrastructure used to define and reason about memory models

See the README.md for more details.