Name		Name	Last commit message	Last commit date
src		src
.gitignore		.gitignore
Dockerfile		Dockerfile
Makefile		Makefile
README.md		README.md
configure		configure

Repository files navigation

CompOptCert on Promising Semantics

This project machanized proofs verifying the correctness of compiler optimization in Coq.

Usage

Requirement: opam (>=2.0.0), Coq 8.13.1
Install dependencies with opam

./configure
make build -j
# clean
make clean

About

Mirror for compcert implementation in promising semantics

plax-lab.github.io/publications/promisingcomp/

0 stars

1 watching

Report repository

Contributors

Languages