Short description is empty for this repo.
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.5.3 and 8.6)
- SSReflect (tested with 1.6.1)
- To compile and test the compiler:
$ cd compiler
$ make CIL build
$ make tests
- To compile Coq proofs:
$ cd proofs
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.
Docker Pull Command