package coq-bedrock2-compiler
A work-in-progress language and compiler for verified low-level programming (compiler part)
Install
Dune Dependency
Authors
Maintainers
Sources
v0.0.9.tar.gz
sha512=6dec4778d54e4276aa81f1252759eb138dfe59ab413384b9a3729dc6c0b5f125aa80a23dc55770369c69f455c14388277e7f5bf3c88b141d8c493cd2d3de92a0
Description
bedrock2 is a low-level systems programming language. This language is equipped with a simple program logic for proving correctness of the programs. This package includes a verified compiler targeting RISC-V from this language.
The project has similar goals as bedrock, but uses a different design. No code is shared between bedrock and bedrock2.
Dependencies (5)
-
zarith
>= "1.11" -
coq-riscv
= "0.0.6" -
coq-bedrock2
= version -
coq
>= "9.0~" -
conf-findutils
build
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page