Research data for "An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic"

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.