This project machanized proofs verifying the correctness of compiler optimization in Coq.
- Requirement: opam (>=2.0.0), Coq 8.13.1
- Install dependencies with opam
./configure
make build -j
# clean
make clean
-
Notifications
You must be signed in to change notification settings - Fork 0
Mirror for compcert implementation in promising semantics
Hughshine/promising-comp
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
Mirror for compcert implementation in promising semantics