This repository contains Rocq and HOL4 developments of a verified bootstrapped compiler for a small imperative language. The compiler is bootstrapped: it can compile itself inside of the ITP, thus removing the need to extract it.
The compiler developments in the two ITPs are available in their corresponding directories, together with ITP-specific instructions:
- HOL4 in
./holwith the starting point in./hol/README.md - Rocq in
./rocqwith the starting point in./rocq/README.md