This repository contains the following subdirectories:
- compiler/ : Compiler from jasmin-lang to assembly.
- proofs/ : Coq implementations of compiler passes / checkers.
- For the compiler: check compiler/README.md
- For the proofs:
- Coq (tested with 8.7.2)
- The Mathematical Components library for Coq (tested with 1.7.0)
- To compile and test the compiler:
$ cd compiler$ make CIL build$ make tests
- To compile Coq proofs:
$ cd proofs$ make
All our code is MIT licensed. Since we use GPL licensed third party Coq theories and extract code from the LGPL licensed Coq standard library, our compiler is GPL licensed.