Coq Formalization for Mininix

Mininix is a smaller version of the Nix expression language. This codebase provides the mechanization of the semantics and reference interpreter for this language in the Coq proof assistant. For more details, I refer to my bachelor's thesis. It should be linked to from the related work section of the Zenodo record after it has been made available on the thesis archive page of iCIS.

Development

During my thesis, I used Nix to manage my Coq installation. If you use Nix, it should be easy to build/check the codebase. If not, this might be a bit more tricky.

There are two things that you need to have installed. The current flake.lock ensures that we have the following software:

Coq, version 8.19.2.
Coq-std++, version 1.10.0.

Using Nix

I have attached a flake.nix and flake.lock file, which should make my setup reproducible. Assuming a working Nix installation with flake support and the Nix command enabled, simply running nix develop should give you a shell where the right Coq and Coq-std++ versions available.

If you have a working direnv installation, simply running direnv allow (after inspecting the .envrc file) should make the right version of Coq and Coq-std++ available.

Without Nix

If you are on some Unix-based system, there is a good chance that your package manager provides a Coq package. The Repology page should give you the information that you need.

You may be able to install Coq-std++ via opam, as described in the README of Coq-std++. However, your operating system's package repositories may also provide a package. Consider taking a look at the Repology pages: coq-stdpp, coq:stdpp.

Building/checking

Running make should run coqc on all files; assuming that you are using a compatible Coq version, this should successfully check all proofs.