diff options
-rw-r--r-- | README.md | 9 |
1 files changed, 6 insertions, 3 deletions
@@ -2,12 +2,15 @@ Coq Formalization for Mininix | |||
2 | ============================= | 2 | ============================= |
3 | 3 | ||
4 | [](https://opensource.org/licenses/BSD-3-Clause) | 4 | [](https://opensource.org/licenses/BSD-3-Clause) |
5 | [](https://doi.org/10.5281/zenodo.12208115) | ||
5 | 6 | ||
6 | Mininix is a smaller version of the Nix expression language. This repository | 7 | Mininix is a smaller version of the Nix expression language. This codebase |
7 | provides the mechanization of the semantics and reference interpreter for this | 8 | provides the mechanization of the semantics and reference interpreter for this |
8 | language in the [Coq](https://coq.inria.fr/) proof assistant. For more details, | 9 | language in the [Coq](https://coq.inria.fr/) proof assistant. For more details, |
9 | I refer to my bachelor' thesis. I will link to it when it is made available on | 10 | I refer to my bachelor's thesis. It should be linked to from the related work |
10 | the [thesis archive](https://www.cs.ru.nl/bachelors-theses/) page of | 11 | section of the [Zenodo record](https://zenodo.org/records/12208115) after it |
12 | has been made available on the [thesis | ||
13 | archive](https://www.cs.ru.nl/bachelors-theses/) page of | ||
11 | [iCIS](https://www.ru.nl/en/institute-for-computing-and-information-sciences). | 14 | [iCIS](https://www.ru.nl/en/institute-for-computing-and-information-sciences). |
12 | 15 | ||
13 | ## Development | 16 | ## Development |