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.

本工件为 AxSL 逻辑的机械化证明开发，其中包含形式化的定义和可由 Coq 证明辅助工具验证的证明。该工件包含了论文中呈现的所有结果。

该项目可以使用 OCaml 构建系统 `dune` 进行编译，且需预先安装相关依赖。构建脚本组织在 `dune-project` 以及若干 `dune` 文件中。

有关在 Docker 环境或手动构建的详细信息，请参阅 `INSTALL.md`。

Coq 开发被组织在两个子目录中。

`theories` 目录包含本工作的主要 Coq 开发。

`system-semantics` 目录包含用于定义和推理内存模型的 Coq 基础设施。

更多详细信息，请参见 `README.md`。